00100	.!SPACES ← "#####################################################" ;
00200	.!HYPHENS ← "--------------------------------------------------------------" ;
00300	.MACRO FRACTION(NUM, DEN) ; ⊂
00400	.TURN ON "{↑↓[]&#" ;
00500	.	N ← "NUM" ; D ← "DEN" ;
00600	.	LN ← LENGTH(N) ; LD ← LENGTH(D) ;
00700	.	IF LN > LD THEN START D ← !SPACES[1 TO (LN-LD) DIV 2] & D ; LMAX ← LN END ;
00800	.	IF LD > LN THEN START N ← !SPACES[1 TO (LD-LN) DIV 2] & N ; LMAX ← LD END ;
00900	.	"↑[{N}]&↓[{D}]&[{(!HYPHENS[1 TO LMAX])}]" ; TURN OFF ; ⊃
01000	
01100	.MACRO SCRIPTS ⊂ TURN ON "↑↓[]&_∪" ⊃
01200	.MACRO GREEKS ⊂ TURN ON "{∂\αβ#←→∞" ⊃
01300	.MACRO FORMAT ⊂ SCRIPTS ; GREEKS ⊃
01400	.MACRO FAC ⊂FILL ADJUST COMPACT CRSPACE GREEKS⊃
01500	
01700	.COUNT SECTION
01800	.MACRO SEC(NAME) ⊂ SECNAME←SSNAME←NULL
01900	.BEGIN SKIP TO COLUMN 1; NEXT SECTION; TURN ON "{∂∞→#"
02000	{!}.##NAME {SKIP
02100	.SECNAME←"NAME"
02200	.SEND CONTENTS ⊂ SKIP
02300	{!}.##NAME\∞ ∞.∞ →#{PAGE!}
02400	. ⊃
02500	.END  ⊃
02600	
02700	.COUNT SUBSECTION IN SECTION PRINTING "!.1"
02800	.MACRO SS(NAME) ⊂ SSNAME←NULL
02900	.BEGIN SKIP TO COLUMN 1; NEXT SUBSECTION; TURN ON "{∂∞→#"
03100	∂8{SUBSECTION!}##NAME{SKIP 1
03150	.SSNAME←"NAME"
03200	.SEND CONTENTS ⊂
03300	∂8{SUBSECTION!}##NAME\∞ ∞.∞ →#{PAGE!}
03400	. ⊃
03500	.END ⊃
03600	
03700	.COUNT SUB2 IN SUBSECTION PRINTING "!.1"
03800	.MACRO SSS(NAME) ⊂
03900	.IF LINES<7 THEN SKIP TO COLUMN 1 ELSE SKIP 1; NEXT SUB2
04000	.BEGIN TURN ON "{∂∞→#"
04100	∂(16){SUB2!}##NAME{SKIP
04200	.SEND CONTENTS ⊂
04300	∂(16){SUB2!}##NAME\∞ ∞.∞ →#{PAGE!}
04400	. ⊃
04500	.END ⊃
04600	
04700	.MACRO BACK ⊂
04800	.PORTION CONTENTS
04900	.COUNT PAGE PRINTING "i"
05000	.FILL NOJUST FORMAT CRBREAK
05050	.SECNAME←SSNAME←NULL
05100	.INDENT 0,30,10 PREFACE 1 TABS 30,33,36,39,42,45,48,51,54,57,60,63
05200	←TABLE OF CONTENTS
05300	.SKIP 2
05400	∂(16)Section→Page
05600	.SECNAME ← "TABLE OF CONTENTS"
05700	.RECEIVE
05800	.		⊃
05900	
06000	.MACRO BV ⊂ SKIP; BEGIN VERBATIM ⊃
06100	
06200	.MACRO FIG(NAME) ⊂ PORTION NAME
06300	.GROUP SKIP 20
06400	←NAME GOES HERE
06500	.	⊃
     

00200	.CENTER CRBREAK GREEKS
00400	
00500	Proposal to
00600	.SKIP 2
00700	THE ADVANCED RESEARCH PROJECTS AGENCY
00800	.SKIP 2
00900	for support of
01000	.SKIP 3
01100	THE STANFORD ARTIFICIAL INTELLIGENCE PROJECT
01200	.SKIP 2
01300	John McCarthy, Professor of Computer Science
01400	Principal Investigator
01500	.SKIP 3
01600	THE HEURISTIC PROGRAMMING PROJECT
01700	.SKIP 2
01800	Edward Feigenbaum, Professor of Computer Science
01900	Co-Principal Investigator
02000	.SKIP
02100	Joshua Lederberg, Professor of Genetics
02200	Co-Principal Investigator
02300	.SKIP 2 }and{ SKIP 1
02400	THE NETWORK PROTOCOL DEVELOPMENT PROJECT
02500	.SKIP 2
02600	Vinton Cerf, Assistant Professor of Computer Science and
02700	Electrical Engineering, Principal Investigator
02800	.SKIP TO LINE 45
02900	January 1973
03000	.SKIP 2
03100	STANFORD UNIVERSITY
     

00100	ABSTRACT
00200	.FAC; BEGIN DOUBLE SPACE; PREFACE 2
00300	Research projects in artificial intelligence, heuristic programming,
00400	and network protocol development are proposed.  These projects will
00500	be administratively distinct within the Computer Science Department
00600	and are described below in separate sections with separate budgets.
00700	The total cost is
00800	$3 million over a period of two years and two weeks (15 June 1973
00900	through 30 June 1975).
01000	
01050	←Artificial Intelligence
01075	
01100	The Stanford Artificial Intelligence Project proposes to advance
01200	existing research programs in robotics, representation theory,
01300	mathematical theory of computation, and automatic deduction.
01400	These activities will cost a total of $1.25 million per year.
01500	
01505	A principal objective of the robotics work will be to lay
01510	foundations in computer vision and manipulation that will
01515	permit major advances in industrial automation.
01520	
01525	The work on representation theory will enlarge the set of
01530	problems that can be represented and, hopefully, solved by
01535	computers.  This field is fundamental to language understanding,
01540	learning from experience, and advanced problem solving.
01545	
01550	Mathematical theory of computation is aimed at formally proving
01555	the correctness of programs.  This will provide a much more
01560	powerful basis for certifying programs than our current imperfect
01562	"debugging" techniques.
01565	
01570	The automatic deduction work will extend heuristic programming
01575	techniques for theorem proving to a wider range of problems
01580	than can now be handled.
01585	
01590	←Heuristic Programming
01595	
01600	The Heuristic Programming Project is planned to continue at a level
01700	of $200,000 per year.
01800	
01805	←Network Protocol Development
01810	
01900	The Network Protocol Development Project has two parts costing a total
01950	of about $50,000 per year.
01975	
01987	The first part
02000	is to provide for the orderly design, development, implementation,
02100	and review of protocols for the ARPA network.  A key element in this
02200	task is to supply theoretical bases for the design of protocols and
02300	to make predictions of performance to be verified by observation and
02400	experiment (e.g. through the Network Measurement Center).
02500	
02600	The second part involves the coordination of an effort to specify
02700	guidelines for subnet and Host-Host protocol design so that it will
02800	be technically feasible for national networks to be interconnected.
02900	The essential problem here is  to  isolate  and  raise  the  critical
03000	issues  which  must  be resolved by the protocols, and to effectively
03100	stimulate and lead the working group's efforts.  The cost of these
03200	activities will be about $50,000 per year.
03300	.END
     

00100	.INSERT CONTENTS
00200	.PORTION MAIN
00300	.PAGE←NULL
00400	.EVERY HEADING({SECNAME},,{SSNAME})
00500	.EVERY FOOTING(,{PAGE!},)
00600	.SEC ARTIFICIAL INTELLIGENCE PROJECT
00700	
00710	Artificial  Intelligence is the experimental and theoretical study of
00732	perceptual and intellectual processes using computers.  Its  ultimate
00754	goal  is to understand these processes well enough to make a computer
00776	perceive, understand and act in ways now only  possible  for  humans.
00788	
00800		The Stanford Artificial Intelligence Project will soon have
00900	been in existence ten years, although the present location and the
01000	computer facilities are a few years newer.  During this time, its work
01100	has been basic and applied research in artificial intelligence and closely
01200	related fields, including computer
01300	vision, problem solving, control of an artificial arm and a vehicle.
01400	This work has been fully described in
01500	our Artificial Intelligence Memoranda and in published
01600	papers.  The bibliography of this proposal gives references [Section 1.6].
01700	Here is a short list of what we consider to have been our main accomplishments.
01800	
01900	Robotics
02000	.NARROW 4,4
02100	
02200	 Development of vision programs for finding, identifying and describing
02300	various kinds of objects in three dimensional scenes.  The scenes include objects with flat
02400	faces and also curved objects.
02500	
02900	 The development of programs for manipulation and assembly of
03000	objects from parts.  The latest result is the complete assembly of an automobile
03100	water pump from parts in known locations.
03200	
03300	.WIDEN
03400	Speech Recognition
03500	
03600	.NARROW 4,4
03700	 Development of a system for recognition of continuous speech, later transferred
03800	to Carnegie-Mellon University and now being expanded upon elsewhere.
03900	  Additional research in speech recognition
04000	has been done here and will continue if support can be found.
04100	
04200	.WIDEN
04300	Heuristic Programming
04400	
04500	.NARROW 4,4
04510	Our support of Hearn's work on symbolic computation led to the development
04532	of REDUCE, now being extended at the University of Utah and widely used
04554	elsewhere.
04576	
04600	 Work in heuristic programming resulting in Luckham's resolution
04700	theorem prover.  This is currently about the best theorem prover in existence, and it
04800	puts us in a position to test the limitations of current ideas about
04900	heuristics so we can go beyond them.
05000	
05100	.WIDEN
05200	Representation Theory
05300	
05400	.NARROW 4,4
05500	 Work in the theory of how to represent information in a computer
05600	is fundamental for heuristic programming, for language understanding
05700	by computers and for programs that can learn from experience.  Stanford
05800	has been the leader in this field.
05900	
06000	.WIDEN
06100	Mathematical Theory of Computation
06200	
06300	.NARROW 4,4
06400	 Our work in mathematical theory of computation is aimed at
06500	replacing debugging by computer checking of proofs that programs
06600	meet their specifications.  McCarthy, Milner, Manna, Floyd, Igarashi,
06700	 and Luckham
06800	have been among the leaders in developing the relevant mathematical
06900	theory, and the laboratory has developed the first actual proof-checking
07000	programs that can check proofs that actual programs meet their specifications.
07100	In particular, Robin Milner's LCF is a practical proof checker for a revised version
07200	of Dana Scott's logic of computable functions.
07300	
07400	.WIDEN
07500	Research Facilities
07600	
07700	.NARROW 4,4
07800	Development of a laboratory with very good computer and program facilities
07900	and special instrumentation for the above areas.  At present, we have the
08000	largest general purpose display-oriented timesharing system in the world.
08100	Unfortunately, it also appears to be the most heavily loaded timesharing
08200	system in the world.
08204	
08220	 The development of a mechanical arm well suited to manipulation research.
08224	It is being copied and used by other laboratories.
08228	
08300	 In the course of developing our facilities, we have improved
08400	LISP, developed an extended Algol compiler called SAIL, written
08500	editors, loaders, and other utility programs for the PDP-10 and made
08600	numerous improvements to time-sharing systems.  Many of these programs,
08604	particularly LISP and SAIL,
08700	are used directly in dozens of other computer centers.
08800	
08900	We have designed an advanced central processor that is about 10 times as
09000	fast as our PDP-10.  We plan to construct this processor and make it
09100	operational within the early part of this proposal period.
09200	
09700	.WIDEN
09800	
09810		In the next period, we propose to continue our work in these areas
09840	with the following expected results:
09870	
09885	.NARROW 4,4
09900	The artificial intelligence problem still won't be conclusively
10000	solved.  As a scientific subject, the study of the mechanisms of
10100	intelligence is as difficult as physics, chemistry, or biology, and decisive
10200	results will be slow in coming and require genius.
10300	
10400	Our identification of intellectual mechanisms and our ability
10500	to make machines carry them out will advance.  The precise results cannot
10600	be predicted.
10700	
10750	.WIDEN
10800		In short term problems and in applications, we can make more
10900	definite predictions:
11000	
11050	.NARROW 4,4
11100	We will lay the groundwork for industrial implementation of automatic
11200	assembly and inspection stations, employing computer vision and general
11300	purpose manipulators.
11700	
11800	We will be able to represent in the computer the full
11900	information required for computer solution of problems such as
12000	the travel problem given in Section 1.1, below.
12100	
12200	We will be able to check proofs of the correctness of actual
12300	though simple compilers into PDP-10 machine language.
12400	.WIDEN
     

00100	.GROUP
02000	The proposed structure of the Project
02100	is given in Figure 1.
02300	
02400	.BV
02500	
02600	          Figure 1.  Structure of the Stanford Artificial 
02700	                        Intelligence Project
02800	
02900	               Principal Investigator:  John McCarthy
03000	                                  |
03100	            ______________________|______________________
03200	           |             |                 |             |
03300	           |             |                 |             |
03400	    _______|_______      |                 |      _______|_______
03500	   |   Computer    |     |                 |     | Mathematical  |
03600	   |   Vision &    |     |                 |     |  Theory of    |
03700	   | Manipulation  |     |                 |     | Computation   |
03800	   |_______________|     |                 |     |_______________|
03900	    Feldman,Binford,     |                 |      McCarthy,Weyhrauch,
04000	      Paul, Quam         |                 |           Luckham
04100	                         |                 |
04200	                         |                 |
04300	                  _______|_______   _______|_______
04400	                 |               | |               |
04500	                 |Representation | |   Automatic   |
04600	                 |    Theory     | |   Deduction   |
04700	                 |_______________| |_______________|
04800	                     McCarthy       Luckham,Green,Allen
04900	.END APART
     

00100	.SS ROBOTICS
00200	
00300	Current research staff:  Jerome Feldman, Tom Binford, Lou Paul, Lynn
00400	Quam, Bruce Anderson, Craig Cook, Randy Davis, Kicha Ganapathy, Gunnar
00500	Grape, Ram Nevatia, Richard Orban, Karl Pingle, Vic Scheinman, Yoram
00600	Yakimovsky.
00700	
00800	During the past several years our  vision  effort  has  shifted  from
00900	simple scenes of polyhedra to complex objects in richer context.  Not
01000	all problems with towers of polyhedra have been solved, but there are
01100	a  host  of  reasons  for moving on.  Manipulation has also proceeded
01200	from manipulation of blocks to assembly operations for  many  of  the
01300	same  reasons.     Minsky and Papert [Minsky 1972] have described the
01400	central  issues  and  the  intellectual  position  of   robotics   in
01500	artificial intelligence. We refer to that discussion as background to
01600	our motivation to direct research to real world scenes  and  objects.
01700	An  important  motivation is to develop applications for manipulation
01800	and visual feedback capabilities which have been developed here.  The
01900	time  is  ready  for  the  first transfer of robotics technology from
02000	laboratory  to  prototype  assembly  stations.  We  discuss  robotics
02100	applications more fully in another section.
02200	
02300	Another  major  motivation is to face new issues; systems have come a
02400	few  steps  toward  heterarchical  systems  from  heirarchy;  from  a
02500	succession  of homogeneous passes with compounding errors to a system
02600	structure where high and low levels interact closely.  One aspect  of
02700	such a system is the use of many functionally independent techniques;
02800	this has meant including  experimentation  with  color  and  texture,
02900	depth  information, motion parallax and image prediction.  The choice
03000	of problems as paradigms is central to the way  in  which  perceptual
03100	systems  evolve.      A  great deal can be done with simple scenes of
03200	polyhedra using a single image  in  one  color,  ignoring  all  other
03300	perceptual abilities.  Since most perceptual problems can be resolved
03400	within  a  single  image,  one   approach   is   to   exhaust   those
03500	possibilities.      Important  areas  are missed; for example, visual
03600	feedback is clumsy without depth information.   For our plans, visual
03700	feedback for manipulation is primary.
03800	
03900	There  are  other  ways  in  which  the  tower  of blocks paradigm is
04000	inadequate  for  our  purposes.      Low  level  feature  description
04100	operators   are   tailored  for  this  case.    Adequate  region  and
04200	edge-oriented descriptors must be evolved.     With  polyhedra,  only
04300	simple  preliminary  grouping  mechanisms have been programmed.  More
04400	intermediate level descriptors must be implemented.
04500	
04600	Although real world scenes are much more  complicated,  they  may  be
04700	simpler  to  perceive in that they have a much richer context.  There
04800	is only very general knowledge available in the  usual  blocks  task;
04900	usually  color,  size,  and  support are unspecified.  In an assembly
05000	task, sizes are known, color is  used  to  code,  and  parts  fit  in
05100	special  ways.     Often  recognition can be based on obvious special
05200	features.  These tasks are good exercise in developing  goal-oriented
05300	visual  systems.  Although development and utilization of intelligent
05400	robots will progress gradually, the information sciences will  impact
05500	industry  enormously  over  a shorter term. An immediate effect is to
05600	streamline information flow in the manufacturing  process.     Simple
05700	systems  can keep track of delayed effects of design decisions, lower
05800	cost of preparation and  transmission,  and  increase  accessibility.
05900	Computer    controlled    scheduling,    resource   allocation,   and
06000	transportation routing are important to most of industrial production
06100	[Anderson  1972].   We see a major contribution from techniques being
06200	pioneered in artificial  intelligence  laboratories,  and  that  such
06300	research  will  have  payoff  throughout  the  entire  development of
06400	intelligent systems. Enormous efficiency  increases  will  come  from
06500	analysis  of  assembly  and  inspection  in  terms of some "primitive
06600	operations".   In the past, computer cost and lack of  sophistication
06700	has  limited  the  ability  for  such  analysis, and the slow pace of
06800	automation has not pressed  hard  for  analysis.    Now  it  will  be
06900	possible   to   find   common  fabrication  and  assembly  operations
07000	throughout a large company, to discover  commonality  in  design  and
07100	components.  The success of that analysis depends upon representation
07200	of fabrication operations and shape.   Representation  is  a  current
07300	concern  in  robotics  labs  and  may  have  early applications. This
07400	orientation to the manufacturing system is already beginning to  have
07500	effect  with  the  "group  technology"  approach,  which  attempts to
07600	describe parts and operations, and group them together in one part of
07700	the   factory.     Until  the  establishment  of  such  analysis  and
07800	commonality  of  operations,  automating  will  be  made  much   more
07900	difficult.
08000	
08100	Considerations are similar for programming automation devices such as
08200	the assembly station we describe.  Even if programming is  difficult,
08300	there  will  be  considerable  applications  for  dexterous  assembly
08400	systems. For example, for the military, it is preferable to stockpile
08500	programs than to stockpile parts or systems for contingency. In batch
08600	production, tapes can be saved to cut stockpiling.   But  to  achieve
08700	full  effect  on  industry, robot systems must be easy to program for
08800	new tasks.  Our current work is concerned  with  strategy  generation
08900	and  automating  visual  feedback.    Time-sharing  systems  will  be
09000	necessary  to  perform  scheduling,  resource   allocation,   routing
09100	operations,  etc.   Thus there is a natural division of labor between
09200	the time-sharing system and small machines. The strategy  generation,
09300	automating   feedback,  and  interactive  system  for  computer-aided
09400	mechanical design expect to reside in the central system.
09500	
09600	A major part of our effort is directed toward the  representation  of
09700	complex  shapes,  for  use  in vision and strategies.  While it might
09800	seem that this effort has only distant applications, for the  reasons
09900	discussed   above,   early   applications   will  be  for  convenient
10000	man/machine   interaction   for   programming    robots    and    for
10100	systematization.   We can expect that in general, much of the work in
10200	symbolic representation of the real world  will  have  early  payoff.
10300	Present  non-intelligent  robots  are programmed by specifying points
10400	along a path  to  be  repeated.    With  computer  control,  optional
10500	trajectories  can  be  executed in case of contingency.  The engineer
10600	must then specify what normal function is, how to monitor it, and how
10700	to  recognize recoverable situations.   To do so, he can specify this
10800	symbolically in interaction with a  program  in  which  he  specifies
10900	normal  and abnormal conditions, shape of parts (usually some variant
11000	of standard parts), the mating of parts for assembly,  and  schematic
11100	descriptions   of  operations  for  insertion  and  inspection.   The
11200	significance of representations in general is to aid these processes.
11300	Our representation provides a natural way of speaking about the shape
11400	of objects, in terms of a structured description of  part/whole  with
11500	primitives  which  resemble many fabrication operations.   The better
11600	the representation, the more it provides intuition for programs as to
11700	the intent of operations and the function of parts.
11800	
11900	A  representation  aids communication in both directions.  We contend
12000	that our representation is important for  computer  graphics.    This
12100	allows  display  of  the  machine's  concepts to the user, and allows
12200	greater use of predictive mechanisms based on internal models.  Input
12300	could  be made visually with a depth measuring system such as we have
12400	been using for the last two years.  Since the operation would be done
12500	on  a central facility, the computer would be adequate for this task.
12600	We expect that the representation will  be  of  considerable  use  in
12700	monocular  vision  also.   We hope to substantiate these predictions.
12800	Another application is  automating  design  of  numerically  machined
12900	parts.    That  will be simplified to the extent that the machine and
13000	the user speak the same language of subparts and their  descriptions.
13100	Benefits  would  come  from  ease  of  programming  and  interaction,
13200	variable  tolerances  for  critical  parts  and   better   monitoring
13300	operations.
13400	
13500	.SSS THE PILOT ASSEMBLY STATION
13600	
13700	We  seek  other  funds  to  partially support application of robotics
13800	techniques to industrial assembly and inspection.   We will implement
13900	over  the  next  few years a prototype assembly station and a support
14000	system for programming the assembly station for its tasks.
14100	
14200	The assembly station is assumed to be normally connected to  a  large
14300	time-shared computer facility. Not only does this appear to be a good
14400	design for our problem, but it is also necessary  for  an  integrated
14500	programmed automation facility.  The only emphasized statement in the
14600	ARPA study report [Anderson  1972]  is:     "The  maximum  impact  of
14700	computers   in  manufacturing  will  come  from  complete,  real-time
14800	computer cognizance and  control  of  all  processes  and  resources,
14900	allowing the precise scheduling and allocation of these resources."
15000	
15100	Each  assembly  station will consist of a small digital computer, one
15200	or more manipulators and cameras. Manipulators and  cameras  will  be
15300	combined  as  modules  in  systems  to suit a given task, and will be
15400	digitally controlled by the station computer.
15500	
15600	The program in the station computer will be flexible as to the number
15700	and  position of manipulators and cameras. It will control input from
15800	the cameras, provide for some pre-processing of the picture  and  the
15900	application  of  simple  tests to the visual data.     In the case of
16000	manipulators it will provide for simultaneous servo control. It  will
16100	also  process  other  inputs,  such  as  from  touch  sensors  on the
16200	manipulators, from photocell interrupt devices, limit switches,  etc.
16300	Both  analog  and binary outputs will be available for the control of
16400	other devices.
16500	
16600	Each station computer will have access to a task  program  specifying
16700	the actions and tests it should perform to carry out its task.   This
16800	task program will be compiled by the central computer.    Compilation
16900	will  consist of the analysis of predicted scenes in order to specify
17000	simple tests that the station computer can carry out, the calculation
17100	of  collision free trajectories for the manipulators, the sequence of
17200	operations and simple contingency plans. etc.  We  are  planning  for
17300	tasks   whose  normal  execution  does  not  require  detailed  scene
17400	analysis.  If scene analysis becomes necessary (e.g. a dropped  part)
17500	we  envision the station sending an image to the central computer for
17600	processing.
17700	
17800	The central computer will perform overall control of  the  individual
17900	assembly  stations  and the relative rates of production.   If at any
18000	station a planned test fails, for which a contingency plan  does  not
18100	exist,  or  any  unexpected  sensor signals are received, the central
18200	computer will also be interrupted and appropriate actions taken.
18300	
18400	Most of the hardware required  for  the  assembly  station  has  been
18500	developed  for  the  laboratory.    Manipulators  and cameras will be
18600	discussed in detail below. The major additional problem is to  refine
18700	the   existing   designs   to  meet  the  demands  of  an  industrial
18800	environment.
18900	
19000	The most difficult part of the assembly station, and the heart of the
19100	of the proposal is a demonstration of the feasibility of the station.
19200	We plan to do this by developing programs which actually assemble and
19300	inspect a variety of fairly complex manufactured items.
19400	
19500	A  typical  example is our current project, assembly of an automobile
19600	water pump. The major  parts  are  to  be  located,  the  screws  are
19700	supplied by a feeder, as is standard.  Locating the body and cover of
19800	the pump require a gross localization, then a  fine  localization  of
19900	screw  holes.      Touch  provides  a  final accuracy and independent
20000	coordination of the hand.   The  placing  of  alignment  pins  within
20100	screw  holes  could  be monitored visually; although in this case,the
20200	previous actions provide adequate accuracy.   Placing  of  the  cover
20300	over  alignment  pins  can  be  carried out without vision.  Improved
20400	force  sensing  now  under  development  will  be  useful  for   that
20500	operation.
20600	
20700	As  we move to more difficult tasks, the sophistication required goes
20800	up quite rapidly.  The  current  manipulation  routines  seem  to  be
20900	expandable  to cover anticipated problems, especially since we intend
21000	to employ special purpose manipulators (tools) for some tasks.    The
21100	main part of our effort will be vision for assembly; an assembly task
21200	will be performed using vision, touch, and two hands.     The  vision
21300	effort  will  be  integrated with other abilities, and while no great
21400	generality will be stressed, new modules will  be  incorporated  into
21500	the  system,  and a set of techniques will evolve.  These will depend
21600	heavily on techniques similar to  those  of  our  recent  studies  in
21700	visual  feedback  and hand/eye coordination [Gill 1972]. The internal
21800	model of the world will be  used  to  predict  visual  appearance  of
21900	selected  areas  of  the  scene, and a set of verification procedures
22000	will confirm or contradict the predictions.  Many of  the  operations
22100	will  be  connected  with  supplying  feedback  to  manipulation, for
22200	alignment and insertion. These visual procedures will have models for
22300	the parts and approximate locations.
22400	
22500	This and other visual tasks connected with assembly will initially be
22600	performed as special case problems.    In  addition,  to  make  these
22700	techniques   available,   we  will  pursue  development  of  strategy
22800	programs.  This step is essential if intelligent assembly devices are
22900	to  be conveniently programmed for complex tasks. Within the division
23000	of labor between large and small machines, this facility must  reside
23100	in  the  central  time-sharing  facility which has large memory, file
23200	storage, and problem-solving languages. The system must have a  model
23300	of  the  parts  for  assembly,and  a  sequence  of  instructions  for
23400	assembly. It will be necessary to have a representation of shape  and
23500	models for usual assembly operations such as insertion and alignment,
23600	and the ability to solve simple problems  in  connection  with  these
23700	operations,  all  this  to  enable  convenient communication with the
23800	user. When these facilities exist, the addition of new  features  and
23900	operations  can be incorporated smoothly, so that users can call on a
24000	growing library of planning modules.  The result of a planning effort
24100	is  a  cycle  of  machine  planning and man-machine interaction which
24200	results in a plan  network  for  the  mini  computer  which  controls
24300	individual machines.
24400	
24500	.SSS RESEARCH IN VISION
24600	
24700	Our  past work on visual feedback [Gill 1972] in stacking objects and
24800	inserting objects  in  holes  is  directly  relevant  to  vision  for
24900	assembly.   The  system provides feedback for picking up, then at the
25000	final position, with the hand still holding the block  and  in  view,
25100	predicts  the  appearance  of edges and corners within a small window
25200	around the faces to be aligned, and  uses  a  corner/edge  finder  to
25300	determine  alignment  error. Incremental motion capability of the arm
25400	is  used  for  error  correction.          That   work   incorporates
25500	self-calibration  to  coordinate  hand and eye coordinate systems and
25600	maintain reliability (by maintaining  calibration),  as  well  as  to
25700	limit   search   by  accurately  predicting  expected  features.  Two
25800	well-developed systems exist to aid future work in  visual  feedback.
25900	GEOMED  [Baumgart 1972a] is a geometric editor which allows the input
26000	of  geometric  models  and  manipulation  of  these  models.   OCCULT
26100	[Baumgart  1972b]  is a hidden line elimination program which gives a
26200	symbolic output, valuable for vision, in a few seconds.
26300	
26400	We have a set of visual  operations  which  provide  confirmation  of
26500	predictions  and  direct  interaction  with the visual image.     For
26600	outdoor scenes, color is an important basis for region  forming,  and
26700	for  preliminary scene organization. Several preliminary color region
26800	analysis programs have been developed [Bajcsy
26900	1972].    These will be extended as described below. An edge operator
27000	[Hueckel 1969,1972] and a region-based corner/edge finder [Gill 1972]
27100	both  operate  on small windows of the scene, as directed by a higher
27200	level.     An edge verifier  is  used  to  confirm  or  reject  edges
27300	predicted  from  context [Tenenbaum 1970].   Color identification has
27400	long been demonstrated.   Recently, a program  has  been  implemented
27500	based  on  Land's Retinex model of color constancy in vision.    This
27600	involves taking intensity measurements with the camera  through  red,
27700	green,  and  blue filter, and setting up a calibration scheme for the
27800	Goethe color triangle in the absence of any external  color  standard
27900	(white).   This is achieved by normalizing the intensities of regions
28000	within the scene through each filter, and defining a  color  triangle
28100	derived  from  this  ordering  data,  with the center of the triangle
28200	designated as white. The regions may then be assigne color  names  in
28300	the  normal  way.   The program as it stands can cope reasonably well
28400	with table top scenes under varied lighting  conditions  -  sunlight,
28500	quartz-halogen  and flourescent, and therefore shows the same kind of
28600	color constancy as do humans.
28700	
28800	We have directed part of our work  to  analysis  of  outdoor  scenes.
28900	Outdoor  scenes were analyzed with a combination of color and texture
29000	region analysis  [Bajcsy  1972];  depth  cues  were  taken  from  the
29100	gradient of texture.  A symbolic representation of texture and of the
29200	world were adopted; descriptors of texture elements were obtained  as
29300	analytic  expressions  from  the  Fourier  spectrum.   A considerable
29400	improvement could be made by combining these techniques with  several
29500	techniques which obtain depth information from correlation of images.
29600	Motion parallax has been used with  a  succession  of
29700	images.   The  successive  images  differ little from one another and
29800	allow local  correlation  without  ambiguity.     In  a  sense,  this
29900	combines the advantages of narrow and wide angle stereo, since stereo
30000	ambiguity is avoided, while large baselines  can  be  accumulated  by
30100	tracking  regions  over  several  images. Another system incorporates
30200	several facilities in wide angle stereo [Quam 1972]; local statistics
30300	are  used  to  limit  search for correspondence of small areas in two
30400	images.    An interesting feature is  self-orientation:    given  two
30500	cameras whose orientation is unknow, the system uses guided search to
30600	establish  a  few  correspondences,  then  determines  the   relative
30700	orientation   of   the   two   cameras.   Such  self-orientation  and
30800	self-calibration  facilities  have  considerable   significance   for
30900	industrial  systems  which can be maintained calibrated.    These are
31000	complementary depth sensing techniques; motion parallax can  be  used
31100	for  planning  paths and characterizing large scale terrain features.
31200	Two camera stereo can be used for  local  manipulation  and  disaster
31300	avoidance.   Visual  feedback  with stereo vision is potentially more
31400	powerful than without.    We have a program  which  has  demonstrated
31500	stereo visual feedback.
31600	
31700	A  thesis  by  Agin  [Agin  1972]  showed  considerable  progress  in
31800	representation and description of complex objects.  He implemented  a
31900	laser  ranging  device [Binford 1970] which was operational two years
32000	ago.    Using depth data and a representation of shape [Binford 1971]
32100	which  we  have developed, we have been able to describe the parts of
32200	objects  like  a  doll,  snake,  and  glove.        The
32300	representation is based on segmenting objects into parts connected at
32400	joints.    Parts  are  described  by  a  volume  representation  with
32500	arbitrary  cross  section defined along a space curve.  The data were
32600	analyzed by techniques suggested by the representation.   Preliminary
32700	segmentation  was made into parts suggested by some primitives of the
32800	representation, smoothly varying,  locally  cylindrical  parts.    An
32900	iterative  procedure  defined  an  approximation  to  the axis of the
33000	segment, fit  circular  cross  sections  normal  to  the  axis,  then
33100	obtained  an  estimate  of  a global cross section function which was
33200	then used to extend the axis and cross section as far as consistent.
33300	
33400	A study of visual and depth ranging techniques has been  carried  out
33500	which  provides  a background for choosing sensors and interface, and
33600	making cost estimates [Earnest 1967, Binford 1972].    An  interesting
33700	result  is  that  the  cost of a laser ranging system such as ours is
33800	less than $1k given a TV system. We have maintained a calibrated hand
33900	and  vision system for several years [Sobel 1970], and have developed
34000	self-calibration  techniques  with  one  and  two  eyes   [Quam 1972,
34100	Gill 1972].
34200	
34300	A  system  for  understanding  scenes of blocks from single views has
34400	been implemented [Falk 1970]; it segments  objects,  matches  against
34500	internal  models,  predicts  appearance  from  its  assumptions,  and
34600	searches for verification and contradiction based  on  the  predicted
34700	image.    Support and spatial relations are also obtained.  There has
34800	been past work on programs  to  obtain  line  drawings  as  input  to
34900	recognition  systems.  An earlier system was based on limited context
35000	of expecting continuation of edges at vertices and predicting missing
35100	edges  in certain expected configurations [Grape 1970]. A more recent
35200	approach has been to use models within the process of generating line
35300	drawings,  so  that  the  most  reasonable next guess can be made and
35400	context used intrinsically in the formation of line drawings.
35500	
35550	.IF LINES<7 THEN NEXT PAGE
35600	←VISUAL DEVELOPMENT FOR ASSEMBLY
35700	
35800	In a later section, we describe assembly of a pump carried  out  with
35900	the  manipulator  using  touch,  without vision.  We are implementing
36000	vision programs to aid the assembly. In  the  pump  assembly,  visual
36100	tasks  consist  of  gross  location  of  large  parts, then using the
36200	information to predict location of images of holes, and monitoring of
36300	insertion  into holes.   These tasks are typical of the simple visual
36400	operations which we will implement or adapt  for  assembly.  We  will
36500	greatly  expand our efforts with visual feedback.  At present, visual
36600	feedback techniques are limited to polyhera.  We will  improve  image
36700	prediction techniques to predict images of objects with curved edges.
36800	We will develop  a  simple  region  analysis  program  which  assumes
36900	adequate contrast to locate the curved edges predicted within a small
37000	window.   Color will be used when necessary.      We  will  implement
37100	two-dimensional  matching  of  boundary curves with predicted curves.
37200	These  will  be  combined  with  our  existing  edge   operator   and
37300	corner/line  operator.     We  will  maintain a calibrated system and
37400	improve calibration updating so that reliability is maintained  at  a
37500	high level.
37600	
37650	.IF LINES<7 THEN NEXT PAGE
37700	←PROPOSED RESEARCH
37800	
37900	We  will improve the laser hardware so that it can be used widely and
38000	extend our work with representation of complex  objects  using  depth
38100	data.     We  are able to make complete descriptions of objects which
38200	consist of a single primitive segment, such as a torus, a snake or  a
38300	cone.     The  programs can segment dolls, toy horses, in intuitively
38400	natural ways [Agin 1972]. It is necessary to improve our segmentation
38500	process  in  order to proceed to joining primitive segments at joints
38600	and make complete descriptions of complex objects.     When  we  have
38700	these  descriptions,  the computer will have symbolic internal models
38800	of objects.   No recognition has yet been done, although we are in  a
38900	position  to  recognize  those  objects which have only one primitive
39000	segment, for which we can make complete descriptions. For recognition
39100	of  more complex objects, once we have complete descriptions, we will
39200	encode the basic properties of the  representation  within  a  visual
39300	memory   scheme   which   allows   access   of  hypothesized  similar
39400	three-dimensional shapes, with  associated  surface  information,  to
39500	compare more closely with extensive verification.  We intend to apply
39600	large parts of our programs for description and recognition of curved
39700	objects  using  only  monocular intensity information. This is a much
39800	harder problem, but within our representation,  shares  much  of  the
39900	same  code,  and  relies  on  the  same  conceptual  basis  of  local
40000	three-dimensional models.
40100	
40200	
40300	We  will  continue  work  on  color region analysis which is based on
40400	proximity rather than contiguity.  This  was  the  plan  outlined  in
40500	previous proposals, and has shown necessary by our work with textured
40600	scenes [Bajcsy 1972].   Another effort combines region analysis  with
40700	a  decision  theoretic approach based on a world model. We anticipate
40800	that these modules will aid the integrated system to function in more
40900	complex  environments than have been attempted in the past.  There is
41000	a growing  effort  on  navigation  of  vehicles  in  outdoor  scenes.
41100	While this is not directly relevant to the industrial environment, it
41200	does reflect the growing involvement in  complex  visual  tasks,  and
41300	will lead to further development of an integrated visual system.
41400	
41500	A  strategy  project  is  underway  dealing with the world of blocks.
41600	The project begins from the idea that robot vision cannot be  studied
41700	except  as a part of intelligent behavior in general.  Visual ability
41800	is FOR something,  and  without  reasonable  expectations  about  the
41900	world,  the  task of seeing is bound to be extremely difficult.    We
42000	plan to implement a system which can  do  simple  manipulation  tasks
42100	("pick  up  the  red  block",  "put  all the cubes in the box") in an
42200	environment of plane-faced objects, and operating in a dialogue mode.
42300	The  system  will have a good but imperfect world model all the time,
42400	and the essence of its ability will be the constant use of this model
42500	to  understand  situations  and  in particular to recover from errors
42600	("Is that block no longer there because the arm  knocked  it  off?").
42700	The  main  point  of  the  project is to find a good organization for
42800	knowledge about the simple world in question:  we  expect  that  when
42900	this  is  done  the  complex  subroutines  of current vision programs
43000	(linefinders etc) will be found to be unnecessarily complex  in  that
43100	they embody in an inefficient way at a low level, knowledge which our
43200	system will contain at a higher level. In part, this will be done  by
43300	expanding  the facilities available.  A stereo vision module is being
43400	programmed, using line  drawings  and  integrating  stereo  with  the
43500	segmentation and recognition processes.
43600	
43700	We  are  at  work  on  a  program which exploits new features of SAIL
43800	[Feldman  1972]  for  dealing   with   multi-process   tasks   in   a
43900	problem-solving environment. The aim is to construct a driver program
44000	to  accomplish  a  simple  assembly  task  under  somewhat  uncertain
44100	conditions.  Making use of the new language features, one can arrange
44200	for such a program to cope with errors in the execution  of  tasks  -
44300	e.g. to recover from dropping things, breaking things, and further to
44400	try several different but possibly cooperative methods for solving  a
44500	problem.   It  is intended that this program will have its own vision
44600	procedures  specially  adapted  for  finding  tools,  e.g.  wrenches,
44700	screwdrivers, etc., and parts, e.g. nuts and bolts. An interpreter is
44800	being developed to allow flexible description  of  the  task  by  the
44900	user.
45000	
45100	.SSS MANIPULATOR DEVELOPMENT
45200	
45300	Manipulator   research  began  at  Stanford  Artificial  Intelligence
45400	Laboratory  in  1965  with  the  acquisition  and  programming  of  a
45500	prototype  Rancho Orthotic Arm.  A later version of this arm was used
45600	in vision directed block stacking programs.
45700	
45800	Our present arm, the result of a continuing design project,  replaced
45900	the  Rancho Arm in 1970. This arm like its predecessor was controlled
46000	by a digital servo program running under the time  sharing  computer.
46100	The new arm was used in the "Instant Insanity" demonstration in 1971.
46200	A second arm of the same type,  with  only  minor  modifications,  is
46300	currently  being interfaced to the computer.   Both arms will share a
46400	common work space and will  be  able  to  be  used  individually,  or
46500	together for two handed tasks.
46600	
46700	Manipulator  research  moves  ahead  simultaneously  on three fronts:
46800	control, primitives and devices.      Tasks are  translated  into  an
46900	existing  hand  language and where the task cannot be accomplished in
47000	terms of existing primitives, new  primitives  are  formulated  in  a
47100	consistent  manner.     When a new primative is formulated, real time
47200	routines are developed to perform the action.  This  also  leads,  in
47300	many  cases,  to  the  development of new hardware.       Also as new
47400	developments occur in hardware design, existing  real  time  routines
47500	are either re-written or modified.
47600	
47700	Research is now concentrating on the following areas:
47800	
47900	Strain gauge instrumentation of the wrist, in order to allow for more
48000	sensitive interaction of the hand with a  task.     High  resolution,
48100	high  sensitivity  touch sensors, to increase tactile recognition and
48200	control abilities.     These developments will lead in  turn  to  new
48300	control concepts.
48400	
48500	Development  of  tools  for the hand. These tools can be instrumented
48600	such that the computer can feel and or see at the end  of  the  tool.
48700	This  should  be  a very important area of research as it goes beyond
48800	present human capabilities.
48900	
49000	Two handed arm control, the planning and execution of tasks requiring
49100	the  coordinated  motion of both arms. This will require an extension
49200	of the existing servo program and  the  analysis  of  synchronization
49300	problems.   The  development of collision avoiders, so that arms will
49400	not collide with other objects and with each other.
49500	
49600	Modification of  the  existing  arm  design  to  provide  for  better
49700	incremental motions, more degrees of freedom and a more rugged design
49800	suitable for industrial use.   Development of arm  and  eye  computer
49900	interfaces.     These  contain synchronized analog/digital converters
50000	for input and current controlled drivers for output.
50100	
50200	The development of new hands is expected as more  complex  tasks  are
50300	attempted.    At present, with only one hand, we have been performing
50400	the positioning type of hand  actions.     When  the  second  arm  is
50500	operational we will be able to perform holding and pulling actions as
50600	well.
50700	
50800	←DEMONSTRATIONS OF MANIPULATION
50900	
51000	Operations controlled by force have been demonstrated  by  turning  a
51100	crank  and  screwing  a  nut  onto  a  bolt.  The  hand  language and
51200	manipulation facilities are shown in the assembly of  a  small  pump.
51300	The  positions of the parts are known approximately; they are located
51400	on a pallet as expected in industrial practice.  By touch,  the  hand
51500	locates  position  and  orientation of the pump body more accurately.
51600	Aligning pins are inserted into the holes to guide the gasket and the
51700	pump  cover.  Screws are obtained from a feeder, as is standard.  All
51800	operations have  been  performed  in  the  assembly,  but  the  total
51900	reliability  is  still  sufficiently  low  that  one error or another
52000	occurs.  Vision has not been used in the assembly.
52100	
52200	.SSS SYSTEM REQUIREMENTS FOR ADVANCED AUTOMATION
52300	
52400	A key element in the development of any large programming  effort  is
52500	the  software  support.   There has been continual effort along these
52600	lines at the Stanford Artificial  Intelligence  Laboratory  and  many
52700	useful  ideas have been developed.  We propose to extend the research
52800	along two separate lines:  support for research and  system  software
52900	for  operating  automated systems.  We will briefly describe our past
53000	efforts in this area and what we propose to undertake.
53100	
53200	The Stanford Artificial  Intelligence  Laboratory  has  pioneered  in
53300	several  areas  of  system  programming,  including  display-oriented
53400	timesharing systems, interactive graphics, and programming languages.
53500	
53600	A great deal of additional effort has gone  into  direct  support  of
53700	hand-eye  research.     Very  early, we established a set of standard
53800	formats and library routines [Pingle 1972a].  A  programming  language,
53900	SAIL, was implemented in 1968.  The language incorporates special
54000	features  for  large real-world-oriented problem solving systems
54100	and is currently in use at a number of  Artificial  Intelligence  and
54200	other laboratories.
54300	
54400	As  we began to assemble larger and more sophisticated collections of
54500	programs, we felt a need  for  flexible  mechanisms  for  cooperating
54600	sequential  processes.  The resulting monitor and language features
54700	[Feldman & Sproull 1971]  have  worked  well  for  us  and  have  been
54800	influential  on  other  projects.      Recently,  we  have  added  an
54900	additional set of features  to  SAIL  [Feldman  1972]  to  facilitate
55000	non-deterministic   and   event-directed  programming.     The  early
55100	reactions to this work, both within the laboratory  and  without  has
55200	been very encouraging.
55300	
55400	
55500	A major share of the programming research effort will be concentrated
55600	on developing a programming system for automated assembly.  This will
55700	combine ideas  from  our  past  work  on  languages,  representation,
55800	computer  graphics and arm control.  We view this task as a branch of
55900	the larger effort on automatic programming being undertaken  in  this
56000	laboratory aad elsewhere.
     

00100	.SSS REFERENCES
00200	.BEGIN INDENT 0,8
00300	[Anderson 1972] R. Anderson, "Programmable Automation, The Future
00400	of Computers in Manufacturing", Datamation, Dec 1972.
00500	
00600	[Agin 1972] G. Agin, "Description and Representation of  Curved  Objects",
00700	Ph.D.  Thesis, Computer Science Dept., Stanford University, September
00800	1972.
00900	
01000	[Bajcsy 1972] "Computer Identification of Visual Texture" Computer Science
01100	Department, Stanford University, (1972).
01200	
01300	[Baumgart 1972a] B. Baumgart, "GEOMED - A Geometric Editor", May 1972.
01400	SAILON-68,Artificial Intelligence Lab, Stanford University,
01500	
01600	[Baumgart 1972b] Baumgart, Bruce G., Winged Edge Polyhedron Representation, 
01700	AIM 179,Artificial Intelligence Lab, Stanford University,October 1972.
01800	
01900	[Binford 1970] T.O.Binford, "Ranging by Laser", Internal Report,
02000	Artificial Intelligence Lab, Stanford University, Oct 1970.
02100	
02200	[Binford 1971] "Visual  Perception  by  Computer",  Invited  paper  at  IEEE Systems
02300	Science and Cybernetics, Miami, Dec 1971.
02400	
02500	[Binford 1972]"Sensor Systems for  Manipulation",  Conference  on  Remotely  Manned
02600	Systems, JPL, Pasadena, Calif, Sept 1972.
02700	
02800	[Earnest 1967] L.D.Earnest,"Choosing an eye for a Computer";
02900	AI Memo 51, Artificial Intelligence Lab, Stanford University, 1967.
03000	
03100	[Falk 1971] G. Falk, "Scene Analysis Based on Imperfect Edge Data", Proc. 2IJCAI,
03200	Brit. Comp. Soc., Sept. 1971.
03300	
03400	[Feldman & Sproull 1971] J.  Feldman  and  R.  Sproull,  "System  Support for the Stanford
03500	Hand-eye System", Proc. 2IJCAI, Brit. Comp. Soc., Sept. 1971.
03600	
03700	[Feldman 1972] J. Feldman, et al,"Recent Developments in SAIL-An Algol Based Language for Artificial 
03800	Intelligence", (with others).  CS 308, Stanford University, August 1972.
03900	To appear in Proc. Fall Joint Computer Conference, 1972.
04000	
04100	[Gill 1972] A, Gill, Visual Feedback and Related Problems in Computer
04200	Controlled Hand-eye Coordination, AIM-178, Stanford AI Laboratory, October 1972.
04300	
04400	[Grape 1969] G. Grape, "Computer Vision through Sequential Abstraction",
04500	Artificial Intelligence Laboratory, Internal Report, 1969.
04600	
04700	[Grape 1970] G. Grape, "On predicting and Verifying Missing Elements in Line-Drawings"
04800	Artificial Intelligence Laboratory, Internal Report, March 1970.
04900	
05000	[Hueckel 1969] M.H. Hueckel, "An Operator Which Locates Edges in Digitized
05100	Pictures",  Stanford  Artificial  Intelligence  Laboratory   AIM-105,
05200	December 1969, JACM, Vol. 18, No. 1, January 1971.
05300	
05400	[Minsky 1972] M. Minsky, "Artificial Intelligence Progress Report", AI Memo 252,
05500	MIT AI Lab, 1972;
05600	
05700	[Paul 1971]  R. Paul,  "Trajectory  Control  of  a  Computer  Arm",  2nd
05800	International Joint Conference on Artificial Intelligence, 1971.
05900	
06000	[Paul 1972] R. Paul, "Modelling, Trajectory Calculation and Servoing of  a
06100	Computer  Controlled  Arm",  Ph.D.   Thesis,  Computer Science Dept.,
06200	Stanford University, Sept. 1972.
06300	
06400	[Pingle   1972a]   Karl   K.  Pingle,  "Hand/Eye  Library",  Stanford
06500	Artificial Intelligence  Laboratory  Operating  Note  35.1,  January,
06600	1972.
06700	
06800	[Pingle  1972b] K.K. Pingle and J.M. Tenenbaum, "An Accomodating Edge
06900	Follower", IJCAI-2. Proceedings of the 2nd.  International  Symposium
07000	on Industrial Robots, May 1972, Chicago, Illinois.
07100	
07200	[Quam 1972] L. H. Quam, S. Liebes, Jr., R. B. Tucker, M.  J.  Hannah,
07300	B.  G.  Eross,  "Computer  Interactive  Picture Processing", Stanford
07400	Artificial Intelligence Laboratory AIM-166, April 1972.
07500	
07600	[Scheinman 1969] V.  D.  Scheinman,  Design  of  a  Computer  Manipulator,
07700	Stanford Artificial Intelligence Project, Memo AIM-92, June 1969.
07800	
07900	[Sobel 1970] Irwin Sobel, "Camera Models and Machine Perception", Stanford
08000	Artificial Intelligence Project Memo AIM-121, May, 1970.
08100	
08200	[Swinehart 1969] D. Swinehart, R.  Sproull,  "SAIL",  Stanford  Artificial
08300	Intelligence Laboratory Operating Note 57, November 1969.
08400	
08500	[Tenenbaum 1970] J. M. Tenenbaum, "Accommodation in Computer Vision",
08600	PhD thesis in Electrical Engineering, September 1970.
08700	.END
     

00100	.SS  MATHEMATICAL THEORY OF COMPUTATION
00200	
00300	Current research staff:  John McCarthy, David Luckham, Robin Milner,
00400	Richard Weyhrauch, Malcolm Newey, Whit Diffie.
00500	
00550	.SSS RECENT ACCOMPLISHMENTS
00600	Recent accomplishments in mathematical theory of computation have
00700	been as follows.
00800	
00900		1. Professor John McCarthy has developed a set of axioms for
01000	the Scott theory in set theory in first order logic.  These axioms
01100	are in the form acceptable to Diffie's first-order-logic proof checker.
01200	
01300		2.  Dr. Jean-Marie Cadiou spent the summer further researching
01400	the difference between the "call by value" and "call by name" methods
01500	of evaluating recursive functions.  This represents further work
01600	in the direction of his thesis [2].
01700	
01800		3.  Dr. David Luckham, Dr. Shigeru Igarashi, and Dr. Ralph
01900	London have together worked on the project of producing a running
02000	program for the correct generation of verification conditions for
02100	the language PASCAL.  This work builds on an idea of C.A.R. Hoare
02200	[3].  
02300		In addition to the verification generation (VG) Dr. Luckham
02400	and J. Morales have used Dr. Luckham's theorem prover to prove
02500	some of the theorems generated by the VG.
02600	
02700		Dr. Luckham has also supervised the thesis of J. Buchanan
02800	[1] in which the notion of a semantic frame has been used to write
02900	programs guaranteed correct by their method of generation.
03000	
03100		4.  Dr. Shigeru Igarashi [4] has explored the question of
03200	extending the notion of the "admissibility" of Scott's computation
03300	induction to a wider class of sentences than considered by Scott.
03400	This work was presented at the MTC Symposium in Novosibirsk, U.S.S.R.
03500	
03600		5.  Dr. Robin Milner and Dr. Richard Weyhrauch completed
03700	their study of definability in LCF.  They produced two papers.  In
03800	[9] LCF was used to express the correctness of programs and a
03900	machine checked proof of the correctness a particular program was
04000	given.  In [8] a proof of the correctness of a compiler was presented.
04100	Dr. Milner also presented an expository paper summerizing all this
04200	work at the Symposium at Novosibirsk [7].  Subsequent to this along
04300	with Dana Scott, work has been done on a version of LCF based on the
04400	type free λ-calculus.  A set of axioms for such a system has been
04500	found.
04600	
04700		6.  Dr. Robin Milner has been studying the theory of processes
04800	using the type free λ-calculus.  This work is still in a preliminary
04900	stage.
05000	
05100		7.  Dr. Richard Weyhrauch has been looking at formal proofs
05200	in several different languages  (first order set theory, first order
05300	logic, LCF) to see if various things learned from LCF carry over to
05400	these languages.
05500	
05600		8.  Malcolm Newey has produced a set of theorems to be used
05700	as a theorem base for people wanting to use LCF.  This includes
05800	axioms for arithmetic, lists and finite sets, as well as about
05900	900 theorems and proofs in these areas.  An A.I. Memo on these will
06000	appear soon.
06100	
06200	.SSS FUTURE WORK
06300	
06400		First there are people working on clarifying the extent of
06500	Floyd's method of inductive assertions.  The main tool for this
06600	study is the embryonic verification generator mentioned above and
06700	Dr. Luckham's theorem prover.  To this end Dr. Luckham is planning an
06800	interactive program that uses both.  The main task here is to
06900	1) demonstrate that the formal system suggested by C.A.R. Hoare,
07000	when extended to the full language PASCAL is correct and useable;
07100	2) program the verification generator (VG), using Hoare's ideas,
07200	to generate seetences, which if provable would guaraatee the
07300	partial correctness of particular programs; 3) use the theorem
07400	prover, perhaps with interactive help, to prove the seetences
07500	generated by the VG.  The work mentioned in 3) is relevant to
07600	this project and are presently continuing.  In addition a new
07700	student, Nori Suzuki, is working on the addition of mechanisms
07800	to the VG to help in proving the termination (or total correctness)
07900	of programs.
08000	
08100		The second project concerns extending the ideas of D. Scott
08200	and C. Strachey.  A major part of this research is a computer program,
08300	LCF, which implements the logical calculus, in which the notions
08400	of "function" and "functional" can be discussed.  Actually there are
08500	now two such calculi, the original LCF [7,8,9] and the type free
08600	logic (5 above).  The following projects are either already underway
08700	or are contemplated in the near future.  A new machine version of
08800	LCF.  This is necessitated for several reasons.  1) The usual run
08900	of features left out; 2) most important a better interface with
09000	other programs.  An examination of how to automate proving of
09100	assertions in LCF.  For example, could the proofs given in [8,9]
09200	have been automated.  Drs. Milner and Weyhrauch have several ideas
09300	along these lines and it is likely that Steve Ness will undertake
09400	this problem as a thesis topic.  Malcolm Newey, another student,
09500	hopes to actually use LCF to prove formally the correctness of
09600	LCOM0 and LCOM4.  An informal proof of their correctness was
09700	presented in [5].  Both of these tasks will require the discussion
09800	of how to create subsidiary deduction rules.  There is also the
09900	question (reflecting on 6 above) of the implementation of a
10000	version of LCF for the type free logic.  Whether this will be done
10100	depends on further theoretical work to show its necessity.
10200	
10300		An atteept to automate either of the above ways of proving
10400	properties of programs requires one to talk about proving theorems
10500	in some formal language.  Another project envisioned is a new
10600	first order logic proof checker which is based on theories of
10700	natural deduction, rather than resolution.  One of the as yet
10800	unexplored discoveries of the work of [8,9] was the effect of
10900	the physical structure of LCF on the feasibility of carrying out
11000	proofs.  Dr. Weyhrauch hopes to examine this question in terms of
11100	natural deduction in general.
11200	
11300		These projects are all directed at the more central
11400	questions, what is the right notion of correctness and equivalence
11500	of programs.  In addition they address themselves to examining
11600	the computational feasibility of automating the procedures
11700	suggested by the theoretical results.  It is hoped that these
11800	studies will eventually lead to a clear notion of correctness that
11900	lends itself to automatic (though perhaps interactive) checking.
12000	
12100	
12200	
12300	
12400	
12500	.SSS REFERENCES
12600	.BEGIN INDENT 0,5
12700		[1]  Buchanan, J., Thesis, to appear
12800	
12900		[2]  Cadiou, J.M., "Recursive definitions of partial functions
13000	and their computations", Stanford Artificial Intelligence Project
13100	AIM-163, March 1972.
13200	
13300		[3]  Hoare, C.A.R., "An axiomatic basis of computer programming",
13400	CACM, Volume 12, 576-80, 583, 1969.
13500	
13600		[4]  Igarashi, S., "Admissibility of fixed-point induction
13700	in first-order logic of typed theories", Stanford Artificial
13800	Intelligence Project, AIM-168, May 1972.
13900	
14000		[5]  London, R.L., "Correctness of two compilers for a LISP
14100	subset", Stanford Artificial Intelligence Project, AIM-151, October
14200	1971.
14300	
14400		[6]  Manna, Z., INTRODUCTION TO MATHEMATICAL THEORY OF
14500	COMPUTATION, Stanford University Computer Science Department
14600	May 1972.
14700	
14800		[7]  Milner, R. (paper given at Novosibirsk), 1972.
14900	
15000		[8]  Milner, R. & Weyhrauch, R., "Proving compiler correctness
15100	in a mechanized logic", Machine Intelligence 7, Michie, E. (ed.),
15200	Edinburgh, Edinburgh University Press, 1972.
15300	
15400		[9]  Weyhrauch, W. & Milner, R., "Program semantics and
15500	correctness in a mechanized logic", First USA-Japan Computer
15600	Conference Proceeedings, Tokyo, Hitashi Printing Company, October
15700	1972.
15800	
15900	.END
     

00100	.SS AUTOMATIC DEDUCTION
00200	
00300	Current research staff:  David Luckham, John Allen, Jack Buchanan
00350	Jorge Morales and Nori Suzuki.
00400	
00500	Research  over  the past year has been directed very strongly towards
00600	developing the applications of automatic proof procedures, especially
00700	in   the  areas  of  mathematical  theorem-proving,  verification  of
00800	computer programs, and automatic generation of programs.   This  work
00900	has  involved  extensive changes and additions to the theorem-proving
01000	program (references include previous A.I. Project reports,and [l,  2,
01100	and  3], and the development of new programs using special features of
01200	the languages MLISP2 [4] and MICRO-PLANNER [5]).  We give  some  brief
01300	details of current work and future plans below.
01400	
01500	Most of these projects have involved the discussion of many  problems
01600	(both  theoretical  and  practical)  in  the  mathematical  theory of
01700	computation, and this has resulted in a  great  deal  of  cooperation
01800	between  the  two  groups of people.  In particular, discussions with
01900	Robin Milner and Richard Weyhrauch  on  their  experiments  with  LCF
02000	helped  the  program  verification  project,  and Richard Weyhrauch's
02100	experiments in proving theorems in various formal systems speeded the
02200	extension  of  user  facilities  in  the  theorem-prover.   Different
02300	projects also turned out to have similar practical problems; e.g. the
02400	simplification algorithms  in  LCF  and  in  the  theorem-prover  are
02500	similar,  and  the  data  files built up by M. Newey for carrying out
02600	proofs in LCF have a significant overlap with the files of facts used
02700	by  J.  Morales  in  the program verification system.  As a result of
02800	this extensive common  ground  of  interests  and  problems,  a  more
02900	integrated  development  of  the  various projects is planned for the
03000	future.
03100	
03200	
03300	.SSS THEOREM PROVING
03400	
03500	The  basis of the theorem-proving effort has been the proof procedure
03600	for first-order logic with equality, originally developed by Allen and Luckham  [1].   This
03700	has been extensively modified by J. Allen in recent months; the basic
03800	theorem-proving program has been speeded up by a  factor  of  20,  an
03900	input-output  language allowing normal mathematical notation has been
04000	added, and the program will select search strategies automatically if
04100	the user wishes (we refer to this as automatic mode).  As a result
04200	it is possible for the program to be used by a person who is  totally
04300	unfamiliar  with  the  theory  of  the  Resolution  principle and its
04400	associated rules of inference and refinements. This program has  been
04500	used  to obtain proofs of several different research announcements in
04600	the Notices of the American Mathematical Society, for example, [6, 7,
04700	and  8].  Recently, (July 1972) J. Morales learned to use the program
04800	essentially by using it to obtain proofs of the results stated in [8,
04900	June 1972] as an exercise. In the course of doing this he was able to
05000	formulate  simple  ways  of using the prover to generate possible new
05100	theorems in the same spirit as  [8],  and  did  in  fact  succeed  in
05200	extending  the  results of [8].  Furthermore, he was able to send the
05300	authors proofs of their results before they had actually had time  to
05400	write  them  up [R.H. Cowen, private correspondence, August 9, 1972].
05500	The prover is also being used as part  of  the  program  verification
05600	system (below).
05700	
05800	At  present  some  modifications  in  the  prover's  standard  search
05900	strategies  are  being  made  by J. Allen.  A version of this program
06000	with user documentation is  being  prepared  for  distribution to other research groups.   The
06100	addition  of  a  language in which the user can specify his intuition
06200	about how a proof of a given statement might possibly be obtained, is
06300	in progress. J. Allen  has  already  programmed  a  very  preliminary
06400	version  of  this  "HUNCH"  language,  and  has completed the systems
06500	debugging necessary  to  get  a  compiled  version  of  J.  Sussman's
06600	CONNIVER  language running here; HUNCH language may be implemented in
06700	CONNIVER, but  discussions  on  this  point  are  not  yet  complete.
06800	Initially,  it is expected that HUNCH language will be useful
06900	in  continuing  with  more  difficult  applications  in   first-order
07000	mathematical  theories.   A  research report outlining the results of
07100	experiments made over the past two years  is  being  prepared  by  J.
07200	Allen  and  D.  Luckham.   A  report  on  J.  Morales' experiments is
07300	available.
07400	
07500	.SSS VERIFICATION OF COMPUTER PROGRAMS
07600	
07700	This project was undertaken jointly by Shigeru Igarashi, Ralph London
07800	and  David  Luckham.   The aim is to construct a system for verifying
07900	automatically  that  a  computer  program  is  consistent  with   its
08000	documentation.   It  was  decided  to  restrict attention to programs
08100	written in N. Wirth's language PASCAL [9] since this was the  subject
08200	of  an  axiomatic  study  by  C.A.R.  Hoare  [10].   Essentially  the
08300	verification system has three main  components,  (i)  a  Verification
08400	Condition  Generator  (VCG),  (ii) a simplifier, and (iii) a theorem-
08500	prover.  A first version of VCG has been implemented in MLISP2; it is
08600	a fairly straightforward encoding of a set of rules of inference that
08700	is  derivation-complete  for  the  system given by Hoare in [10]. VCG
08800	will accept  a  PASCAL  program  (including  go  to's,  conditionals,
08900	while's,  procedure  and  function calls with certain restrictions on
09000	the types of the actual parameters of procedure calls,  and  arrays),
09100	together  with  a  documentation,  and  will output a set of "lemmas" or
09200	conditions that, if provable, will ensure that  relative  consistency
09300	holds  true.   The  simplifier,  which  is  to process the conditions
09400	output by VCG, has not yet been written.  Initially,  proofs  of  the
09500	conditions  for  simple arithmetical programs and for certain sorting
09600	programs involving array operations, were obtained by D. Luckham and J. Allen
09700	using the theorem-proving  program.  A more systematic
09800	series of experiments in which proofs of verification conditions were
09900	obtained from standard data files using the prover in automatic mode,
10000	have been made by J. Morales.
10100	
10200	These  experiments are continuing.  It is planned to add new rules of
10300	inference to the theorem-prover and  to  add  some  simple  debugging
10400	strategies  for  pointing  out  possible relative inconsistencies.  A
10500	more flexible version of VCG is planned which will allow the user  to
10600	specify  his  own  rules  of  inference  for  an extension of Hoare's
10700	system.  A preliminary version of the simplifier is essential if  the
10800	whole  verification  process  is  to  be made fully automatic for any
10900	reasonable class of programs.  People currently engaged in this  work
11000	include  D. Luckham,  J. Morales,  N. Suzuki,  and  R. London (latter
11100	at ISI, University of Sourthern California).  A research report  on  VCG  is  being  prepared  by
11150	S. Igarashi and R. London and D. Luckham.
11300	
11400	
11500	.SSS AUTOMATIC PROGRAM GENERATION
11600	
11700	We mention this work briefly here since it  is  an  outgrowth  of  an
11800	attempt to extend the applicability of the theorem-prover to problems
11900	in Artificial Intelligence, and makes use of a particular notion of a
12000	problem  environment  (called  a "semantic frame") which was designed
12100	for that original purpose.  However, the system as it now stands,  is
12200	best thought of as a heuristic theorem-prover for a subset of Hoare's
12300	logical system.  It has been implemented in LISP using the  backtrack
12400	features  of  Micro-Planner,  by  J.  Buchanan. It accepts as input a
12500	problem environment and a problem and, if successful, gives as output
12600	a  program  for  solving  the  problem.   At  the  moment, the output
12700	programs  are composed of the primitive operators of the environment,
12800	assignments,  conditional  branches,   while's,   and   non-recursive
12900	procedure  calls.   This system has been used to generate progams for
13000	solving various  problems  to  do  with  robot  control,  conditional
13100	planning,  and  for  computing  arithmetical  functions.   A research
13200	report outlining the logical basis for the  system  and  its  overall
13300	capabilities  is  in  preparation by D. Luckham and J. Buchanan.  The
13400	details of its implementation will be available  in  J.R.  Buchanan's
13500	Ph.D. Thesis (also in preparation).
13600	
13700	
13800	.SSS REFERENCES
13900	.BEGIN INDENT 0,5
14000	[1]  John Allen and David Luckham (1970), An Interactive Theorem-
14100	     Proving Program, Proc. Fifth International Machine Intelligence
14200	     Workshop, Edinburgh University Press, Edinburgh.
14300	
14400	[2]  Richard B. Kieburtz and David Luckham, "Compatibility and
14500	     Complexity of Refinements of the Resolution Principle",
14600	     SIAM J. Comput., Vol. 1, No. 4, December 1972.
14700	
14800	[3]  David Luckham and Nils J. Nilsson, "Extracting Information
14900	     from Resolution Proof Trees", Artificial Intelligence, Vol. 2,
15000	     No. 1, pp. 27-54, Spring 1971.
15100	
15200	[4]  David C. Smith, "MLISP", Computer Science Department, Artificial
15300	     Intelligence Memo No. AIM-135, October 1970.
15400	
15500	[5]  Sussman and R. Winograd, Micro Planner Manual, Project MAC.
15600	
15700	[6]  Chinthayamma (1969), Sets of Independent Axioms for a Ternary
15800	     Boolean Algebra, Notices Amer. Math. Soc., 16, p. 654.
15900	
16000	[7]  E.L. Marsden, "A Note on Implicative Models", Notices Amer.
16100	     Math. Soc. No. 682-02-7, p. 89, January 1971.
16200	
16300	[8]  Robert H. Cowen, Henry Frisz, Alan Grenadir, "Some New
16400	     Axiomatizations in Group Theory", Preliminary Report, Notices
16500	     Amer. Math. Soc., No. 72T-112, p. A547, June 1972.
16600	
16700	[9]  N. Wirth, "The Programming Language PASCAL", ACTA Informatica
16800	     I 1., p. 35-63, 1971.
16900	
17000	[10] C.A.R. Hoare, "An Automatic Approach to Computer Programming",
17100	     Commun ACM. 12, 10 576-580, 583, October 1969.
17200	.END
     

00100	.SS FACILITIES
00200	
00300	The computer  facilities  of  the  Stanford  Artificial  Intelligence
00400	Laboratory include the following equipment.
00500	
00600	.BEGIN VERBATIM
00700	Central Processors:  Digital Equipment Corporation PDP-10 and PDP-6
00800	
00900	Primary Store:       65K words of 1.7 microsecond DEC Core
01000		             65K words of 1 microsecond Ampex Core
01100	                     131K words of 1.6 microsecond Ampex Core
01200	
01300	Swapping Store:      Librascope disk (5 million words, 22 million
01400	                     bits/second transfer rate)
01500	
01600	File Store:          IBM 3330 disc file, 6 spindles (leased)
01700	
01800	Peripherals:         4 DECtape drives, 2 magnetic tape drives
01900		             (7 track), line printer, Calcomp plotter,
02000			     Xerox Graphics Printer
02100	
02200	Terminals:           58 TV displays, 6 III displays, 3 IMLAC
02300		             displays, 1 ARDS display, 15 Teletype terminals.
02400	
02500	Special  Equipment:  Audio  input  and  output  systems, hand-eye
02600	                     equipment (2 TV cameras, 3 arms), remote-
02700	                     controlled cart
02800	.END
02900	The facility operates nearly 24 hours of  every  day.   It  typically
03000	carries  a  load of forty-some jobs throughout the day and seldom has
03100	less than eight active users all night long.
03200	
03300	It is expected that the new  high  speed  processor  currently  being
03400	fabricated  in  our  laboratory  will  become  the  main  timesharing
03500	processor during the early part of the proposal period.  This  should
03600	provide  adequate  computational  support  for  the proposed research
03700	program.
03800	
03900	It will be necessary to purchase  some  special  instrumentation  and
04000	peripheral  computer equipment in support of our research in computer
04100	vision and manipulation.  Thus, $75,000 per year  has  been  budgeted
04200	for capital equipment, based on recent experience.
     

00050	.SS PROJECT PUBLICATIONS
00100	.SSS RECENT ARTICLES AND BOOKS
00200	.BEGIN COUNT REF FROM 1 TO 100; AT ">>" ⊂ APART GROUP NEXT REF; REF!}.∂5 {⊃
00300	
00400	Articles and books by members of the Stanford Artificial Intelligence
00500	Laboratory are listed below.
00600	.INDENT 0,5
00700	
00800	>> E. Ashcroft and Z. Manna,"Formalization of Properties of Parallel Programs",
00900	  Machine Intelligence 6, Edinburgh Univ. Press, 1971.
01000	
01100	>> E. Ashcroft and Z. Manna, "The Translation of `Go To' Programs to `While'
01200	 Programs", Proc. IFIP Congress 1971.
01300	
01400	>> K. M. Colby, S. Weber, F. D. Hilf, "Artificial Paranoia", J. Art. Int.,
01500	Vol. 2, No. 1, 1971.
01600	
01700	>> G. Falk, "Scene Analysis Based on Imperfect Edge Data", Proc.
01800	 2IJCAI, Brit. Comp. Soc., Sept. 1971.
01900	
02000	>> J. A. Feldman and A. Bierman, "A Survey of Grammatical Inference",
02100	  Proc. International Congress on Pattern Recognition, Honolulu,
02200	  January 1971, also in S, Watanbe (ed.), FRONTIERS OF PATTERN
02300	  RECOGNITION, Academic Press, 1972.
02400	
02500	>> J. Feldman and R. Sproull, "System Support for the Stanford
02600	 Hand-eye System", Proc. 2IJCAI, Brit. Comp. Soc., Sept. 1971.
02700	
02800	>> J. Feldman, et al, "The Use of Vision and Manipulation to Solve
02900	 the `Instant Insanity' Puzzle", Proc. 2IJCAI, Brit. Comp. Soc.,
03000	 Sept. 1971.
03100	
03200	>> R. W. Floyd, "Toward Interactive Design of Correct Programs",
03300	  Proc. IFIP Congress 1971, pp. 1-5.
03400	
03500	>> A. Hearn, "Applications of Symbol Manipulation in Theoretical
03600	 Physics", Comm. ACM, August 1971.
03700	
03800	>> F. Hilf, K. Colby, D. Smith, W. Wittner, W. Hall,
03900	  "Machine-Mediated Interviewing", J. Nervous & Mental Disease,
04000	  Vol. 152, No. 4, 1971.
04100	
04200	>> M. Hueckel, "An Operator which Locates Edges in Digitized
04300	  Pictures", JACM, January 1971.
04400	
04500	>> M. Kahn and B. Roth, "The Near-minimum-time Control of Open-loop
04600	 Articulated Kinematic Chains", Trans. ASME, Sept. 1971.
04700	
04800	>> R. Kling, "A Paradigm for Reasoning by Analogy", Proc. 2IJCAI,
04900	 Brit. Comp. Soc., Sept. 1971.
05000	
05100	>> D. Knuth, "An Empirical Study of FORTRAN Programs", Software --
05200	  Practice and Experience, Vol. 1, 105-133, 1971.
05300	
05400	>> D. Luckham and N. Nilsson, "Extracting Information from Resolution
05500	Proof Trees", Artificial Intelligence Journal, Vol. 2, No. 1, pp. 27-54,
05600	June 1971.
05700	
05800	>> Z. Manna (with R. Waldinger), "Toward Automatic Program Synthesis",
05900	  Comm. ACM, March 1971.
06000	
06100	>> Z. Manna, "Mathematical Theory of Partial Correctness", J. Comp.
06200	 & Sys. Sci., June 1971.
06300	
06400	>> R. Milner, "An Algebraic Definition of Simulation between
06500	 Programs", Proc. 2IJCAI, Brit. Comp. Soc., Sept. 1971.
06600	
06700	>> U. Montanari, "On the Optimal Detection of Curves in Noisy
06800	  Pictures", Comm. ACM, May 1971.
06900	
07000	>> N. Nilsson, "Problem-solving Methods in Artificial Intellegence",
07100	  McGraw-Hill, New York, 1971.
07200	
07300	>> R. Paul, "Trajectory Control of a Computer Arm", Proc. 2IJCAI,
07400	 Brit. Comp. Soc., Sept. 1971.
07500	
07600	>> K. Pingle and J. Tenenbaum, "An Accomodating Edge Follower",
07700	 Proc. 2IJCAI, Brit. Comp. Soc., Sept. 1971.
07800	
07900	>> B. Roth, "Design, Kinematics, and Control of Computer-controlled
08000	  Manipulators", Proc. 6th All Union Conference on New Problems in
08100	  Theory of Machines & Mechanics, Leningrad, Jan. 1971.
08200	
08300	>> R. Schank, "Finding the Conceptual Content and Intention in an
08400	 Utterance in Natural Language Conversation", Proc. 2IJCAI, Brit.
08500	 Comp. Soc., 1971.
08600	
08700	>> J. Tenenbaum, et al, "A Laboratory for Hand-eye Research", Proc.
08800	 IFIP Congress, 1971.
     

00100	>> A. W. Biermann and J. A. Feldman, "On the Synthesis of Finite-state Machines from Samples
00200	  of Their Behavior", IEEE Transactions on Computers, Vol. C-21, No. 6,
00300	  pp. 592-596, June 1972.
00400	
00500	>> A. W. Biermann, "On the Inference of Turing Machines from Sample
00600	Computations", Artificial Intelligence J., Vol. 3, No. 3, Fall 1972.
00700	
00800	>> J. M. Cadiou and Z. Manna, "Recursive Definitions of Partial Functions
00900	and their Computations", ACM SIGPLAN Notices, Vol. 7, No. 1, January 1972.
01000	
01100	>> K. M. Colby, F. D. Hilf, S. Weber, and H. C. Kraemer, "Turing-like
01200	Indistinguishability Tests for the Validation of a Computer Simulation
01300	of Paranoid Processes", Artificial Intelligence J., Vol. 3, No. 3, Fall 1972.
01400	
01500	>> G. Falk, "Interpretation of Imperfect Line Data as a Three-Dimensional
01600	Scene", J. Artificial Intelligence, Vol. 3, No. 2, 1972.
01700	
01800	>> J. A. Feldman, "Some Decidability Results on Grammatical Inference
01900	  and Complexity", Information and Control, Vol. 20, No. 3, pp. 244-262,
02000	  April 1972.
02100	
02200	>> J. A. Feldman, J. R. Low, D. C. Swinehart, and R. H. Taylor, "Recent
02300	  Developments in SAIL, an ALGOL-based language for Artificial
02400	  Intelligence", Proc. Fall Joint Computer Conference, 1972.
02500	
02600	>> S. J. Garland and D. C. Luckham, "Translating Recursive Schemes into
02700	Program Schemes", ACM SIGPLAN Notices, Vol. 7, No. 1, January 1972.
02800	
02900	>> J. Gips, "A New Reversible Figure", Perceptual & Motor Skills, 34, 306, 1972.
03000	
03100	>> Richard B. Kieburtz and David Luckham, "Compatibility and Complexity
03200	of Refinements of the Resolution Principal", SIAM J. Comput., Vol. 1, No. 4,
03300	December 1972.
03400	
03500	>> D. E. Knuth, "Ancient Babylonian Algorithms", Comm. ACM, July 1972.
03600	
03700	>> R. L. London, "Correctness of a Compiler for a LISP Subset", ACM SIGPLAN
03800	Notices, Vol. 7, No. 1, January 1972.
03900	
04000	>> Z. Manna, S. Ness, and J. Vuillemin, "Inductive Methods for Proving
04100	Properties of Programs", ACM SIGPLAN Notices, Vol. 7, No. 4, January 1972.
04200	
04300	>> Z. Manna and J. Vuillemin, "Fixpoint Approach to the Theory of
04400	Computation", Comm. ACM, July 1972.
04500	
04600	>> R. Milner, "Implementatiion and Application of Scott's Logic for Computable
04700	Functions", ACM SIGPLAN NOTICES, Vol. 7, No. 1, January 1972.
04800	
04900	>> James A. Moorer, "Music and Computer Composition", Comm. ACM, January
05000	1972.
05100	.APART END
     

00050	.SKIP TO COLUMN 1
00100	.SSS THESES
00200	
00300	Theses that have been published by the Stanford Artificial Intelligence
00400	Laboratory are listed here.  Several earned degrees at institutions
00500	other than Stanford, as noted.
00600	
00700	.BEGIN INDENT 0,7;
00800	AIM-43, R. Reddy, AN  APPROACH  TO  COMPUTER  SPEECH  RECOGNITION  BY
00900	     DIRECT  ANALYSIS  OF  THE  SPEECH WAVE, Ph.D. Thesis in Computer
01000	     Science, September 1966.
01100	
01200	AIM-46, S. Persson, SOME SEQUENCE EXTRAPOLATING PROGRAMS:  A STUDY OF
01300	     REPRESENTATION  AND  MODELING IN INQUIRING SYSTEMS, Ph.D. Thesis
01400	     in  Computer  Science,  University  of   California,   Berkeley,
01500	     September 1966.
01600	
01700	AIM-47,  B. Buchanan, LOGICS OF SCIENTIFIC DISCOVERY, Ph.D. Thesis in
01800	     Philosophy, University of California, Berkeley, December 1966.
01900	
02000	AIM-44, J.  Painter,  SEMANTIC  CORRECTNESS  OF  A  COMPILER  FOR  AN
02100	     ALGOL-LIKE  LANGUAGE,  Ph.D.   Thesis in Computer Science, March
02200	     1967.
02300	
02400	AIM-56, W. Wichman, USE OF OPTICAL FEEDBACK IN THE  COMPUTER  CONTROL
02500	     OF AN ARM, Eng. Thesis in Electrical Engineering, August 1967.
02600	
02700	AIM-58,  M. Callero, AN ADAPTIVE COMMAND AND CONTROL SYSTEM UTILIZING
02800	     HEURISTIC  LEARNING  PROCESSES,  Ph.D.   Thesis  in   Operations
02900	     Research, December 1967.
03000	
03100	AIM-60,   D.   Kaplan,   THE  FORMAL  THEORETIC  ANALYSIS  OF  STRONG
03200	     EQUIVALENCE FOR ELEMENTAL PROPERTIES, Ph.D. Thesis  in  Computer
03300	     Science, July 1968.
03400	
03500	AIM-65, B. Huberman, A PROGRAM TO PLAY CHESS END GAMES, Ph.D.  Thesis
03600	     in Computer Science, August 1968.
03700	
03800	AIM-73, D.  Pieper, THE KINEMATICS  OF  MANIPULATORS  UNDER  COMPUTER
03900	     CONTROL, Ph.D. Thesis in Mechanical Engineering, October 1968.
04000	
04100	AIM-74,  D. Waterman, MACHINE LEARNING OF HEURISTICS, Ph.D. Thesis in
04200	     Computer Science, December 1968.
04300	
04400	AIM-83, R.  Schank, A  CONCEPTUAL  DEPENDENCY  REPRESENTATION  FOR  A
04500	     COMPUTER  ORIENTED  SEMANTICS,  Ph.D.   Thesis  in  Linguistics,
04600	     University of Texas, March 1969.
04700	
04800	AIM-85, P.  Vicens, ASPECTS OF SPEECH RECOGNITION BY COMPUTER,  Ph.D.
04900	     Thesis in Computer Science, March 1969.
05000	
05100	AIM-92,   Victor   D.    Scheinman,  DESIGN  OF  COMPUTER  CONTROLLED
05200	     MANIPULATOR, Eng. Thesis in Mechanical Engineering, June 1969.
05300	
05400	AIM-96, Claude Cordell Green, THE APPLICATION OF THEOREM  PROVING  TO
05500	     QUESTION-ANSWERING   SYSTEMS,   Ph.D.     Thesis  in  Electrical
05600	     Engineering, August 1969.
05700	
05800	AIM-98, James J.  Horning, A STUDY OF  GRAMMATICAL  INFERENCE,  Ph.D.
05900	     Thesis in Computer Science, August 1969.
06000	
06100	AIM-106,  Michael E. Kahn, THE NEAR-MINIMUM-TIME CONTROL OF OPEN-LOOP
06200	     ARTICULATED  KINEMATIC  CHAINS,  Ph.D.   Thesis  in   Mechanical
06300	     Engineering, December 1969.
06400	
06500	AIM-121, Irwin Sobel, CAMERA MODELS  AND  MACHINE  PERCEPTION,  Ph.D.
06600	     Thesis in Electrical Engineering, May 1970.
06700	
06800	AIM-130,  Michael  D.   Kelly,  VISUAL  IDENTIFICATION  OF  PEOPLE BY
06900	     COMPUTER, Ph.D. Thesis in Computer Science, July 1970.
07000	
07100	AIM-132, Gilbert Falk, COMPUTER INTERPRETATION OF IMPERFECT LINE DATA
07200	     AS  A  THREE-DIMENSIONAL  SCENE,  Ph.D.   Thesis  in  Electrical
07300	     Engineering, August 1970.
07400	
07500	AIM-134, Jay Martin  Tenenbaum,  ACCOMMODATION  IN  COMPUTER  VISION,
07600	     Ph.D. Thesis in Electrical Engineering, September 1970.
07700	
07800	AIM-144,  Lynn H. Quam, COMPUTER COMPARISON OF PICTURES, PhD Thesis in
07900	     Computer Science, May 1971.
08000	
08100	AIM-147, Robert E. Kling, REASONING BY ANALOGY WITH APPLICATIONS TO
08200	     HEURISTIC PROBLEM SOLVING:  A CASE STUDY, PhD Thesis in Computer
08300	     Science, August 1971.
08400	
08500	AIM-149, Rodney Albert Schmidt, Jr., A STUDY OF THE REAL-TIME CONTROL
08600	     OF A COMPUTER-DRIVEN VEHICLE, PhD Thesis in Electrical Engineering,
08700	     August 1971.
08800	
08900	AIM-155, Jonathan Leonard Ryder, HEURISTIC ANALYSIS OF LARGE TREES AS
09000	     GENERATED IN THE GAME OF GO, PhD Thesis in Computer Science,
09100	     December 1971.
09200	
09300	AIM-163, J.M. Cadiou, RECURSIVE DEFINITIONS OF PARTIAL FUNCTIONS  AND
09400	     THEIR COMPUTATIONS, PhD Thesis in Computer Science, April 1972.
09500	
09600	AIM-173, Gerald Jacob Agin, REPRESENTATION AND DESCRIPTION OF CURVED
09700	     OBJECTS, PhD Thesis in Computer Science, October 1972.
09800	
09900	AIM-174, Morris, Francis Lockwood, CORRECTNESS OF TRANSLATIONS OF
10000	     PROGRAMMING LANGUAGES--AN ALGEBRAIC APPROACH, PhD Thesis in
10100	     Computer Science, August 1972.
10200	
10300	AIM-177, Paul, Richard, MODELLING, TRAJECTORY CALCULATION AND SERVOING
10400	     OF A COMPUTER CONTROLLED ARM, PhD Thesis in Computer Science,
10500	     (forthcoming)
10600	
10700	AIM-178, Gill, Aharon, VISUAL FEEDBACK AND RELATED PROBLEMS IN COMPUTER
10800	     CONTROLLED HAND EYE COORDINATION, PhD Thesis in Electrical
10900	     Engineering, October 1972.
11000	
11100	AIM-180, Bajcsy, Ruzena, COMPUTER IDENTIFICATION OF TEXTURED VISIUAL
11200	     SCENES, PhD Thesis in Computer Science, October 1972.
11300	.END
     

00100	.SKIP TO COLUMN 1
00200	.SSS FILM REPORTS
00300	
00400	Prints of the following film reports are available for loan to interested
00500	groups.
00700	.BEGIN VERBATIM
00750	
00800	1.  Art Eisenson and Gary Feldman, "Ellis D. Kroptechev and Zeus, his
00900	      Marvelous  Time-Sharing  System",  16mm  black  and  white with
01000	      sound, 15 minutes, March 1967.
01100	
01200	The advantages of time-sharing over  standard  batch  processing  are
01300	revealed  through the good offices of the Zeus time-sharing system on
01400	a PDP-1 computer.  Our hero, Ellis, is saved from a fate  worse  than
01500	death.   Recommended for mature audiences only.
01600	
01700	2.  Gary Feldman, "Butterfinger", 16mm color with sound,  8  minutes,
01800	      March 1968.
01900	
02000	Describes  the  state  of  the  hand-eye  system  at  the  Artificial
02100	Intelligence Project in the fall of 1967.  The PDP-6 computer getting
02200	visual information  from  a  television  camera  and  controlling  an
02300	electrical-mechanical  arm  solves  simple  tasks  involving stacking
02400	blocks.  The techniques of recognizing the blocks and their positions
02500	as well as controlling the arm are briefly presented.  Rated "G".
02600	
02700	3.  Raj Reddy, Dave Espar and Art Eisenson, "Hear Here",  16mm  color
02800	      with sound, 15 minutes, March 1969.
02900	
03000	Describes the state of the speech recognition project as  of  Spring,
03100	1969.  A discussion of the problems of speech recognition is followed
03200	by two real time demonstrations of the  current  system.   The  first
03300	shows the computer learning to recognize phrases and second shows how
03400	the hand-eye system may be controlled by voice commands.  Commands as
03500	complicated  as  "Pick  up  the  small  block  in  the lower lefthand
03600	corner", are recognized and the tasks are carried out by the computer
03700	controlled arm.
03800	
03900	4.  Gary Feldman and Donald Peiper, "Avoid", 16mm  silent,  color,  5
04000	      minutes, March 1969.
04100	
04200	Reports on a computer program written by  D.  Peiper  for  his  Ph.D.
04300	Thesis.    The   problem   is   to   move   the  computer  controlled
04400	electrical-mechanical arm through a space filled  with  one  or  more
04500	known  obstacles.   The  program  uses  heuristics for finding a safe
04600	path; the film demonstrates the  arm  as  it  moves  through  various
04700	cluttered environments with fairly good success.
04800	
04900	5.  Richard Paul and Karl Pingle, "Instant Insanity",  16  mm  color,
05000	      silent, 6 minutes, August, 1971.
05100	
05200	Shows the hand/eye system  solving  the  puzzle  "Instant  Insanity".
05300	Sequences  include  finding  and recognizing cubes, color recognition
05400	and object manipulation.  This film was made  to  accompany  a  paper
05500	presented  at  the  1971 International Joint Conference on Artificial
05600	Intelligence in London.  It may  be  hard  to  understand  without  a
05700	narrator.
05800	
05900	6.  Suzanne Kandra, "Motion and  Vision",  16  mm  color,  sound,  22
06000	      minutes, November 1972.
06100	
06200	A  technical  presentation  of  three  research projects completed in
06300	1972:  advanced arm control by R. P. Paul [AIM-177],  visual feedback
06400	control  by  A. Gill [AIM-178], and representation and description of
06500	curved objects by G. Agin [AIM-173].
06600	.END
     

00100	.SKIP TO COLUMN 1
00200	.SSS RECENT REPORTS
00300	
00400	Abstracts of recent Artificial Intelligence Memos are given below.
00500	
00600	.BEGIN VERBATIM
00700	                                1971
00800	
00900	AIM-140,   Roger   C.   Schank,   INTENTION,   MEMORY,  AND  COMPUTER
01000		UNDERSTANDING, January 1971, 59 pages.
01100	
01200	Procedures  are  described for discovering the intention of a speaker
01300	by relating the Conceptual Dependence representation of the speaker's
01400	utterance to the computer's world model such that simple implications
01500	can be made.  These procedures function at levels higher than that of
01600	structure of the memory.  Computer understanding of natural  language
01700	is  shown  to consist of the following parts:  assigning a conceptual
01800	representation to an  input;  relating  that  representation  to  the
01900	memory such as to extract the intention of the speaker; and selecting
02000	the correct response type triggered by such an utterance according to
02100	the situation.
02200	
02300	AIM-141,  Bruce  G.  Buchanan,  Edward  A.  Feigenbaum,  and   Joshua
02400		Lederberg,  THE  HEURISTIC  DENDRAL   PROGRAM  FOR EXPLAINING
02500		EMPIRICAL DATA, February 1971, 20 pages.
02600	
02700	The Heuristic DENDRAL program uses an information processing model of
02800	scientific   reasoning   to  explain  experimental  data  in  organic
02900	chemistry. This report summarizes the organization and results of the
03000	program  for  computer scientists.  The program is divided into three
03100	main parts: planning, structure generation, and evaluation.
03200	
03300	The planning phase infers constraints on the search  space  from  the
03400	empirical  data  input to the system.  The structure generation phase
03500	searches a tree whose termini are models  of  chemical  models  using
03600	pruning  heuristics of various kinds.  The evaluation phase tests the
03700	candidate structures against  the  original  data.   Results  of  the
03800	program's analyses of some tests are discussed.
03900	
04000	AIM-142,  Robin Milner, AN ALGEBRAIC DEFINITION OF SIMULATION BETWEEN
04100		PROGRAMS, February 1971, 21 pages.
04200	
04300	A  simulation  relation  between  programs  is   defined   which   is
04400	quasi-ordering.    Mutual simulation is then an equivalence relation,
04500	and by dividing out by it we abstract from a program such details  as
04600	how  the  sequencing  is controlled and how data is represented.  The
04700	equivalence classes are approximations to the  algorithms  which  are
04800	realized, or expressed, by their member programs.
04900	
05000	A  technique  is  given  and  illustrated  for proving simulation and
05100	equivalence of programs; there is an analogy with  Floyd's  technique
05200	for   proving   correctness  of  programs.   Finally,  necessary  and
05300	sufficient conditions for simulation are given.
05400	
05500	AIM-143.  John McCarthy, Arthur Samuel  and  Artificial  Intelligence
05600		Project staff,  Edward  Feigenbaum   and   Heuristic  Dendral
05700		Project  staff,    PROJECT  TECHNICAL  REPORT,   MARCH  1971,
05800		80 pages, (out of print).
05900	
06000	An  overview  is  presented  of  current  research  at  Stanford   in
06100	artificial  intelligence  and  heuristic programming.  This report is
06200	largely the text of a proposal  to  the  Advanced  Research  Projects
06300	Agency for fiscal years 1972-3.
06400	
06500	AIM-144.  Lynn H. Quam, COMPUTER COMPARISON OF PICTURES,   May  1971,
06600		120 pages.
06700	
06800	This   dissertation  reports  the  development  of  digital  computer
06900	techniques  for  detecting  changes  in  scenes  by  normalizing  and
07000	comparing  pictures  which were taken from different camera positions
07100	and under different conditions  of  illumination.  The  pictures  are
07200	first  geometrically normalized to a common point of view.  Then they
07300	are photometrically normalized to eliminate the  differences  due  to
07400	different   illumination,  camera  characteristics,  and  reflectance
07500	properties of the scene due to different sun and view angles.   These
07600	pictures  are  then  geometrically registered by maximizing the cross
07700	correlation  between  areas  in  them.   The  final  normalized   and
07800	registered pictures are then differenced point by point.
07900	
08000	The  geometric  normalization  techniques require relatively accurate
08100	geometric models for the camera and the  scene,  and  static  spatial
08200	features  must  be present in the pictures to allow precise geometric
08300	alignment using the technique of cross correlation maximization.
08400	
08500	Photometric normalization also requires a relatively  accurate  model
08600	for  the  photometric response of the camera, a reflectance model for
08700	the scene (reflectance as a function of the  illumination  view,  and
08800	phase  angles)  and  some  assumptions about the kinds of reflectance
08900	changes which are to be detected.
09000	
09100	These techniques have been incorporated in  a  system  for  comparing
09200	Mariner 1971 pictures of Mars to detect variable surface phenomena as
09300	well as color and polarization  differences.   The  system  has  been
09400	tested using Mariner 6 and 7 pictures of Mars.
09500	
09600	Although the techniques described in this dissertation were developed
09700	for Mars pictures, their use is  not  limited  to  this  application.
09800	Various  parts  of  this  software  package,  which was developed for
09900	interactive use on the time-sharing system of the Stanford Artificial
10000	Intelligence Project, are currently being applied to other scenery.
10100	
10200	
10300	AIM-145,  Bruce  G.  Buchanan,  Edward  A.  Feigenbaum,  and   Joshua
10400		Lederberg, A HEURISTIC PROGRAMMING STUDY OF THEORY  FORMATION
10500		IN SCIENCE, June 1971, 41 pages.
10600	
10700	The Meta-DENDRAL program is a a  vehicle  for  studying  problems  of
10800	theory formation in science.  The general strategy of Meta-DENDRAL is
10900	to reason from data to plausible generalizations and then to organize
11000	the  generalizations  into  a unified theory.  Three main subproblems
11100	are discussed: (1) explain the experimental data for each  individual
11200	chemical structure, (2) generalize the results from each structure to
11300	all structures, and (3) organize the generalizations into  a  unified
11400	theory.   The  program  is  built  upon  the  concepts and programmed
11500	routines already  available  in  the  Heuristic  DENDRAL  performance
11600	program,  but  goes  beyond  the performance program in attempting to
11700	formulate the theory which the performance program will use.
11800	
11900	
12000	AIM-146, Andrei P. Ershov, PARALLEL PROGRAMMING, July 1971, 14 pages.
12100	
12200	This  report is based on lectures given at Stanford University by Dr.
12300	Ershov in November, 1970.
12400	
12500	
12600	AIM-147,  Robert  E. Kling, REASONING BY ANALOGY WITH APPLICATIONS TO
12700		HEURISTIC  PROBLEM  SOLVING:   A  CASE  STUDY,   August 1971,
12800		191 pages.
12900	
13000	An  information-processing  approach  to  reasoning  by  analogy   is
13100	developed  that  promises  to  increase  the  efficiency of heuristic
13200	deductive problem-solving systems.  When a deductive  problem-solving
13300	system accesses a large set of axioms more than sufficient particular
13400	problem,  it  will  often  create  many  irrelevant  deductions  than
13500	saturate the memory of the problem solver.
13600	
13700	Here,  an  analogy  with  some  previously  solved  problem and a new
13800	unsolved problem is used to restrict the data base to a small set  of
13900	appropriate  axioms.  This procedure (ZORBA) is studied in detail for
14000	a resolution theorem proving system.  A set of  algorithms  (ZORBA-I)
14100	which  automatically  generates  an  analogy  between  a new unproved
14200	theorem, T↓A, and a previously proved theorem,  T,  is  described  in
14300	detail. ZORBA-I is implemented in LISP on a PDP-10.
14400	
14500	ZORBA-I is examined in terms of its empirical performance on parts of
14600	analogous theorems drawn from abstract algebra.   Analytical  studies
14700	are  included  which show that ZORBA-I can be useful to aid automatic
14800	theorem proving in many pragmatic cases while it may be  a  detriment
14900	in certain specially contrived cases.
15000	
15100	
15200	AIM-148, Edward Ashcroft, Zohar Manna,  and  Amir  Pneuli,  DECIDABLE
15300		PROPERTIES OF MONADIC FUNCTIONAL SCHEMAS,  July  1971,
15400		10 pages.
15500	
15600	We  define  a  class  of  (monadic) functional schemas which properly
15700	include `Ianov' flowchart schemas.  We  show  that  the  termination,
15800	divergence and freedom problems for functional schemas are decidable.
15900	Although it is possible  to  translate  a  large  class  of  non-free
16000	functional  schemas  into equivalent free functional schemas, we show
16100	that this  cannot  be  done  in  general.   We  show  also  that  the
16200	equivalence  problem  for free functional schemas is decidable.  Most
16300	of  the  results  are  obtained from  well-known  results  in  Formal
16400	Languages and Automata Theory.
16500	
16600	
16700	AIM-149, Rodney Albert Schmidt, Jr., A STUDY OF THE REAL-TIME CONTROL
16800		OF A COMPUTER-DRIVEN VEHICLE, August 1971, 180 pages.
16900	
17000	Vehicle  control  by  the  computer  analysis  of  visual  images  is
17100	investigated.   The  areas  of  guidance,  navigation,  and  incident
17200	avoidance  are  considered.  A television camera is used as the prime
17300	source of visual image data.
17400	
17500	In the guidance system developed for an experimental vehicle,  visual
17600	data  is  used to gain information about the vehicle system dynamics,
17700	as well as to guide the vehicle.  This information is  used  in  real
17800	time  to  improve performance of the non-linear, time-varying vehicle
17900	system.
18000	
18100	A scheme for navigation by pilotage through the  recognition  of  two
18200	dimensional  scenes  is developed.  A method is proposed to link this
18300	to a computer-modelled map in order to make journeys.
18400	
18500	Various difficulties in avoiding anomolous incidents in the automatic
18600	control  of  automobiles are discussed, together with suggestions for
18700	the application of this  study  to  remote  exploration  vehicles  or
18800	industrial automation.
18900	
19000	
19100	AIM-150, Robert  W.  Floyd,  TOWARD  INTERACTIVE  DESIGN  OF  CORRECT
19200		PROGRAMS, September 1971, 12 pages.
19300	
19400	We  propose  an  interactive  system  proving  the  correctness  of a
19500	program, or locating errors, as the program is designed.
19600	
19700	AIM-151, Ralph L. London, CORRECTNESS OF TWO  COMPILERS  FOR  A  LISP
19800		SUBSET, October 1971, 41 pages.
19900	
20000	Using  mainly  structural induction, proofs of correctness of each of
20100	two running  Lisp  compilers  for  the  PDP-10  computer  are  given.
20200	Included  are the rationale for presenting these proofs, a discussion
20300	of the proofs, and the changes  needed  to  the  second  compiler  to
20400	complete its proof.
20500	
20600	
20700	AIM-152, A.W. Biermann, ON THE  INFERENCE  OF  TURING  MACHINES  FROM
20800		SAMPLE COMPUTATIONS, October 1971, 31 pages.
20900	
21000	An  algorithm is presented which when given a complete description of
21100	a set of Turing machine computations finds a Turing machine which  is
21200	capable of doing those computations.  This algorithm can serve as the
21300	basis for designing a trainable  device  which  can  be  trained   to
21400	simulate  any  Turing machine by being led through a series of sample
21500	computations done by that machine.  A  number of examples  illustrate
21600	the  use  of  the technique and the possibility of the application to
21700	other types of problems.
21800	
21900	
22000	AIM-153,  Patrick J. Hayes, THE FRAME PROBLEM AND RELATED PROBLEMS IN
22100		ARTIFICIAL INTELLIGENCE, November 1971, 18 pages.
22200	
22300	The frame problem arises in considering the logical  structure  of  a
22400	robot's beliefs.  It has been known for some years, but only recently
22500	has much progress been made.  The problem is described and discussed.
22600	Various   suggested  methods  for  its  solution  are  outlines,  and
22700	described in a uniform notation.   Finally,  brief  consideration  is
22800	given  to  the  problem  of  adjusting a belief system in the face of
22900	evidence which contradicts beliefs.  It is shown that a variation  on
23000	the  situation  notation  of  (McCarthy  and  Hayes, 1969) permits an
23100	elegant approach, and relates this problem to the frame problem.
23200	
23300	
23400	AIM-154,  Zohar  Manna,  Stephen  Ness  and Jean Vuillemin, INDUCTIVE
23500		METHODS  FOR  PROVING  PROPERTIES OF PROGRAMS, November 1971,
23600		24 pages.
23700	
23800	We  have  two  main  purposes  in  this paper.  First, we clarify and
23900	extend  known  results  about  computation  of  recursive   programs,
24000	emphasizing  the  difference  between  the  theoretical and practical
24100	approaches.  Secondly, we present and examine various  known  methods
24200	for  proving  properties of recursive programs.  We discuss in detail
24300	two  powerful  inductive   methods,   computational   induction   and
24400	structural  induction,  illustrating  their  applications  by various
24500	examples. We also briefly discuss some other related methods.
24600	
24700	Our aim in this work is to introduce inductive methods to as  wide  a
24800	class  of  readers  as  possible  and  to  demonstrate their power as
24900	practical  techniques.  We  ask   the   forgiveness   of   our   more
25000	theoretical-minded  colleagues  for  our occasional choice of clarity
25100	over precision.
25200	
25300	
25400	AIM-155, Jonathan Leonard Ryder, HEURISTIC ANALYSIS OF LARGE TREES AS
25500		GENERATED IN THE GAME OF GO, December 1971, 300 pages.
25600	
25700	The  Japanese  game  of  Go  is  of  interest  both  as  a problem in
25800	mathematical repesentation and as a game which generates a move  tree
25900	with  an  extraordinarily  high branching factor (100 to 300 branches
26000	per ply).  The complexity of Go (and the difficulty of Go  for  human
26100	players)  is  thought  to be considerably greater than that of chess.
26200	The constraints of being able to play a complete game  and  of  being
26300	able to produce a move with a moderate amount of processing time were
26400	placed on the solution.
26500	
26600	The basic approach  used  was  to  find  methods  for  isolating  and
26700	exploring  several  sorts  of relevant subsections of the global game
26800	tree.  This process depended heavily on the  ability  to  define  and
26900	manipulate  the  entities of Go as recursive functions rather than as
27000	patterns of stones. A general machine-accessible  theory  of  Go  was
27100	developed to provide context for program evaluations.
27200	
27300	A  program  for  playing  Go  is now available on the Stanford PDP-10
27400	computer.  It will play a  complete  game,  taking  about  10  to  30
27500	seconds for an average move.  The quality of play is better than that
27600	of a beginner in many respects, but incompletenesses in  the  current
27700	machine-representable  theory  of Go prevent the present program from
27800	becoming a strong player.
27900	
28000	
28100	AIM-156,  Kenneth Mark Colby, Franklin Dennis Hilf, Sylvia Weber, and
28200		Helena C. Kraemer,  A  RESEMBLANCE TEST  FOR  THE  VALIDATION
28300		OF   A   COMPUTER   SIMULATION   OF   PARANOID     PROCESSES,
28400		November 1971, 29 pages.
28500	
28600	A computer simulation of paranoid processes in the form of a dialogue
28700	algorithm  was  subjected to a validation study using an experimental
28800	resemblance test in which judges rate  degrees of paranoia present in
28900	initial  psychiatric  interviews  of  both  paranoid  patients and of
29000	versions of the paranoid model.  The statistical results  indicate  a
29100	satisfactory   degree  of  resemblance  between  the  two  groups  of
29200	interviews. It is concluded that  the  model  provides  a  successful
29300	simulation of naturally occuring paranoid processes.
29400	
29500	
29600	AIM-157, Yorick Wilks, ONE SMALL HEAD -- SOME REMARKS ON THE  USE  OF
29700		`MODEL' IN LINGUISTICS, December 1971, 17 pages.
29800	
29900	I argue that the present situation in formal linguistics, where  much
30000	new  work  is presented as being a "model of the brain", or of "human
30100	language behavior", is  an  undesirable  one.   My  reason  for  this
30200	judgement  is  not  the  conservative  (Braithwaitian)  one  that the
30300	entities in question are not  really  models  but  theories.   It  is
30400	rather that they are called models because they cannot be theories of
30500	the brain at the present stage of brain research, and hence that  the
30600	use  of  "model"  in  this  context  is  not  so much aspirational as
30700	resigned about our total  ignorance  of  how  the  brain  stores  and
30800	processes   linguistic   information.  The  reason  such  explanatory
30900	entities cannot be theories is  that  this  ignorance  precludes  any
31000	"semantic  ascent" up the theory; i.e., interpreting the items of the
31100	theory in terms of observables.  And the brain items,  whatever  they
31200	may  be,  are  not,  as  Chomsky  has  sometimes claimed, in the same
31300	position as the "occult entities" of Physics  like  Gravitation;  for
31400	the brain items are not theoretically unreachable, merely unreached.
31500	
31600	I  then  examine  two  possible  alternate  views  of what linguistic
31700	theories should be proffered as theories of:   theories  of  sets  of
31800	sentences, and theories of a particular class of algorithms.  I argue
31900	for a form of the latter view, and that  its  acceptance  would  also
32000	have the effect of making Computational Linguistics a central part of
32100	Linguistics, rather than the poor relation it is now.
32200	
32300	I examine a distinction among "linguistic models"  proposed  recently
32400	by   Mey.   who   was   also  arguing  for  the  self-sufficiency  of
32500	Computational Linguistics, though as a "theory  of  performance".   I
32600	argue  that  his  distinction  is  a  bad one, partly for the reasons
32700	developed above and partly because he attempts to tie it to Chomsky's
32800	inscrutable  competance-performance distinction.  I conclude that the
32900	independence and self-sufficiency of  Computational  Linguistics  are
33000	better supported by the arguments of this paper.
33100	
33200	
33300	AIM-158, Zohar Manna, Ashok Chandra, PROGRAM SCHEMAS  WITH  EQUALITY,
33400		December 1971, 22 pages.
33500	
33600	We discuss the class  of  program  schemas  augmented  with  equality
33700	tests,  that  is, tests of equality between terms.  In the first part
33800	of the paper we illustrate the "power" of equality tests.   It  turns
33900	out  that the class of program schemas with equality is more powerful
34000	than  the  "maximal"  classes   of   schemas   suggested   by   other
34100	investigators.  In  the  second  part  of  the  paper, we discuss the
34200	decision problems of program schemas with equality. It is shown,  for
34300	example,  that  while  the  decision problems normally considered for
34400	schemas (such as halting, divergence,  equivalence,  isomorphism  and
34500	freedom)   are   decidable   for  ianov  schemas.   They  all  become
34600	undecidable  if  general  equality  tests  are  added.   We  suggest,
34700	however,  limited  equality  tests  which  can  be  added  to certain
34800	subclasses of program schemas  while  preserving  their  decidability
34900	property.
35000	
     

00100	                                1972
00200	
00300	
00400	AIM-159,  J.A.  Feldman  and  Paul  C.  Shields, TOTAL COMPLEXITY AND
00500		INFERENCE OF BEST PROGRAMS, April 1972.
00600	
00700	Axioms  for  a  total  complexity  measure  for abstract programs are
00800	presented. Essentially, they require  that  total  complexity  be  an
00900	unbounded  increasing  function  of  the Blum time and size measures.
01000	Algorithms for finding the  best  program  on  a  finite  domain  are
01100	presented,   and   their   limiting  behavior  for  infinite  domains
01200	described.  For total complexity, there are important senses in which
01300	a machine can find the best program for a large class of functions.
01400	
01500	
01600	AIM-160,  J. Feldman, AUTOMATIC PROGRAMMING, February 1972, 20 pages.
01700	
01800	The revival of interest in Automatic Programming is  considered.  The
01900	research  is divided into direct efforts and theoretical developments
02000	and the successes and prospects of each are described.
02100	
02200	
02300	AIM-161, Y. Wilks, AN ARTIFICIAL  INTELLIGENCE  APPROACH  TO  MACHINE
02400		TRANSLATION, February 1972, 44 pages.
02500	
02600	The paper describes a system of  semantic  analysis  and  generation,
02700	programmed  in  LISP  1.5  and designed to pass from paragraph length
02800	input in English to French via  an  interlingual  representation.   A
02900	wide class of English input forms will be covered, but the vocabulary
03000	will initially be restricted to one of a  few  hundred  words.   With
03100	this  subset  working,  and  during the current year (1971-72), it is
03200	also hoped to map the interlingual representation onto some predicate
03300	calculus notation so as to make possible the answering of very simple
03400	questions about the translated  matter.   The  specification  of  the
03500	translation system itself is complete, and its main points are:
03600	i) It translates phrase by  phrase--with  facilities  for  reordering
03700	phrases  and  establishing  essential semantic connectivities between
03800	them--by mapping complex semantic stuctures of  "message"  onto  each
03900	phrase.  These  constitute  the  interlingual  representation  to  be
04000	translated.  This matching is done without  the  explicit  use  of  a
04100	conventional  syntax  analysis,  by taking as the appropriate matched
04200	structure the "most dense" of  the  alternative  structures  derived.
04300	This  method  has been found highly successful in earlier versions of
04400	this analysis system.
04500	
04600	ii) The French output strings are generated without the explicit  use
04700	of  a  generative  grammar.   That  is  done by means of STEREOTYPES:
04800	strings of French words, and functions evaluating  to  French  words,
04900	which are attached to English word senses in the dictionary and built
05000	into the interlingual representation by the analysis  routines.   The
05100	generation  program thus receives an interlingual representation that
05200	already contains both  French  output  and  implicit  procedures  for
05300	assembling  the output, since the stereotypes are in effect recursive
05400	procedures specifying the content and production of the  output  word
05500	strings.   Thus  the  generation  program  at no:time consults a word
05600	dictionary or inventory of grammar rules.
05700	
05800	It  is  claimed that the system of notation and translation described
05900	is a convenient one for expressing and handling the items of semantic
06000	information that are ESSENTIAL to any effective MT system.  I discuss
06100	in some detail the semantic information needed to ensure the  correct
06200	choice  of output prepositions in French; a vital matter inadequately
06300	treated by virtually all previous formalisms and projects.
06400	
06500	
06600	AIM-162, Roger Schank, Neil Goldman, Chuck  Reiger,  Chris  Reisbeck,
06700		PRIMITIVE    CONCEPTS    UNDERLYING    VERBS    OF   THOUGHT,
06800		April 1972, 102  pages.
06900	
07000	In  order  to  create  conceptual  structures  that will uniquely and
07100	unambiguously represent the meaning of an utterance, it is  necessary
07200	to  establish  `primitive'  underlying  actions and states into which
07300	verbs can be mapped.  This paper presents analyses of the most common
07400	mental  verbs in terms of such primitive actions and states. In order
07500	to represent the way people speak about their  mental  processes,  it
07600	was  necessary  to  add  to  the  usual ideas of memory structure the
07700	notion of Immediate Memory.  It is then argued that  there  are  only
07800	three primitive mental ACTs.
07900	
08000	
08100	AIM-163, J.M. Cadiou, RECURSIVE DEFINITIONS OF PARTIAL FUNCTIONS  AND
08200		THEIR COMPUTATIONS, April 1972, 160 pages.
08300	
08400	A formal syntactic and semantic model  is  presented  for  `recursive
08500	definitions'  which  are  generalizations of those found in LISP, for
08600	example.   Such  recursive  definitions  can  have  two  classes   of
08700	fixpoints,  the  strong  fixpoints  and  the weak fixpoints, and also
08800	possess a class of computed partial functions.
08900	
09000	Relations between these classes are presented:  fixpoints  are  shown
09100	to  be  extensions  of  computed  functions.   More precisely, strong
09200	fixpoints are shown to be extensions of computed functions  when  the
09300	computations   may   involve  "call  by  name"  substitutions;  weak
09400	fixpoints are shown to be extensions of computed functions  when  the
09500	computation  only  involve  "call  by  value"   substitutions.    The
09600	Church-Rosser  property for recursive definitions with fixpoints also
09700	follows from these results.
09800	
09900	Then conditions are given on the recursive definitions to ensure that
10000	they possess least fixpoints (of both classes), and computation rules
10100	are given for computing these two fixpoints:  the "full"  computation
10200	rule,  which  leads  to  the least weak fixpoint.  A general class of
10300	computation rules, called `safe innermost', also lead to  the  latter
10400	fixpoint.   The "leftmost innermost" rule is a special case of those,
10500	for the LISP recursive definitions.
10600	
10700	
10800	AIM-164,  Zohar Manna  and  Jean  Vuillemin, FIXPOINT APPROACH TO THE
10900		THEORY OF COMPUTATION, April 1972, 29 pages. 
11000	
11100	Substantial effort has been put into finding verification  techniques
11200	for  computer programs. There are now so many verification techniques
11300	that a choice in a practical situation may appear  difficult  to  the
11400	non-specialist.  In particular, the most widely used methods, such as
11500	the  "inductive  assertion  method",  can  be  used  to  prove   some
11600	input-output  relation  (assuming  that the program terminates) while
11700	such  problems  as  termination  or  equivalence  usually  require  a
11800	different type of technique.
11900	
12000	Our  main purpose in this paper is to suggest that Scott's fixedpoint
12100	approach to the semantics of programming languages frees us from that
12200	dilemma.  It allows one not only to justify all existing verification
12300	techniques, but also to extend them to  handle  other  properties  of
12400	computer  programs,  including  termination  and  equivalence,  in  a
12500	uniform manner.
12600	
12700	AIM-165, D.A. Bochvar, TWO  PAPERS  ON  PARTIAL  PREDICATE  CALCULUS,
12800		April 1972, 50 pages.
12900	
13000	The three-valued system to which this study is devoted is of interest
13100	as a logical calculus  for  two  reasons:   first,  it  is  based  on
13200	formalization  of  certain  basic  and  intuitively obvious relations
13300	satisfied by the predicates  "true",  "false"  and  "meaningless"  as
13400	applied  to  propositions,  and  as  a  result the system possesses a
13500	clear-cut  and  intrinsically  logical  interpretation;  second,  the
13600	system  provides  a  solution  to  a  specifically  logical  problem,
13700	analysis  of  the  paradoxes  of  classical  mathematical  logic,  by
13800	formally proving that certain propositions are meaningless.
13900	
14000	The  paper  consists  of  three  parts.   In the first we develop the
14100	elementary part of the  system--the  propositional  calculus--on  the
14200	basis of intuitive considerations.  In the second part we outline the
14300	"restricted" functional calculus corresponding to  the  propositional
14400	calculus.   The third and last part uses a certain "extension" of the
14500	functional  calculus  to   analyze   the   paradoxes   of   classical
14600	mathematical logic.
14700	
14800	We  are  indebted to Professor V.I. Glivenko for much valuable advice
14900	and criticism.  In particular, he provided a more suitable definition
15000	of the function a(see I, Section 2, subsection 1.).
15100	
15200	AIM 166, Lynn H. Quam, Sidney Liebes, Jr., Robert B.  Tucker,  Marsha
15300		Jo  Hannah,  Botond G. Eross,   COMPUTER  INTERACTIVE PICTURE
15400		PROCESSING, April 1972, 40 pages.
15500	
15600	This  report  describes  work  done  in  image  processing  using  an
15700	interactive  computer  system.  Techniques for image differencing are
15800	described and examples using images returned from Mars by the Mariner
15900	Nine  spacecraft are shown.  Also described are techniques for stereo
16000	image processing.  Stereo processing  for  both  conventional  camera
16100	systems and the Viking 1975 Lander camera system is reviewed.
16200	
16300	AIM-167,  Ashok  Chandra,  EFFICIENT  COMPILATION OF LINEAR RECURSIVE
16400		PROGRAMS, June 1972, 43 pages.
16500	
16600	We  consider  the  class  of  linear  recursive  programs.   A linear
16700	recursive program is a set of procedures  where  each  procedure  can
16800	make   at   most   one   recursive   call.   The  conventional  stack
16900	implementation of recursion requires time and space both proportional
17000	to  n,  the  depth  of  recursion.    It  is  shown  that in order to
17100	implement linear recursion so as to execute in  time  n  one  doesn't
17200	need space proportional to n:  n**ε for sufficiently small ε will do.
17300	It is also known that with constant space one  can  implement  linear
17400	recursion  in  time  n**2.   We  show  that  one  can do much better:
17500	n**(1+ε) for arbitrarily small ε.  We also describe an algorithm that
17600	lies between these two:  it takes time n*log n and space log n.
17700	
17800	It  is  shown that several problems are closely related to the linear
17900	recursion problem, for example, the problem  of  reversing  an  input
18000	tape given a finite automaton with several one-way heads.  By casting
18100	all these problems  into  canonical  form,  efficient  solutions  are
18200	obtained simultaneously for all.
18300	
18400	AIM-168,  Shigeru Igarashi, ADMISSIBILITY OF FIXED-POINT INDUCTION IN
18500		FIRST-ORDER LOGIC OF TYPED THEORIES, May 1972, 40 pages.
18600	
18700	First-order logic is extended so as  to  deal  with  typed  theories,
18800	especially  that  of  continuous functions with fixed-point induction
18900	formalized by D. Scott.  The translation of his formal system, or the
19000	λ calculus-oriented system derived and implemented by R. Milner, into
19100	this logic amounts to adding predicate calculus features to them.
19200	
19300	In such a logic the fixe∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈∧␈ebra to computing  are  compatible:  the  semantic
29400	function  provided  by interpreting ("running") one binary relational
29500	algebra on another is a homomorphism on  an  operator  algebra  whose
29600	elements are binary relational algebras.
29700	
29800	Using these mathematical tools, proofs can be provided systematically
29900	of the correctness of compilers for fragmentary programming languages
30000	each embodying a single language  "feature".   Exemplary  proofs  are
30100	given   for  statement  sequences,  arithmetic  expressions,  Boolean
30200	expressions, assignment statements, and while  statement.   Moreover,
30300	proofs of this sort can be combined to provide (synthetic) proofs for
30400	in principle, many different  complete  programming  languages.   One
30500	example of such a synthesis is given.
30600	
30700	
30800	AIM-175, Tanaka, Hozumi, HADAMARD TRANSFORM FOR SPEECH WAVE ANALYSIS,
30900	         August 1972, 34 pages.
31000	          (forthcoming)
31100	
31200	Two methods of speech wave analysis using the Hadamard transform  are
31300	discussed.   The first method is a direct application of the Hadamard
31400	transform for speech waves.   The  reason  this  method  yields  poor
31500	results  is  discussed.   The second method is the application of the
31600	Hadamard transform to a log-magnitude frequency spectrum.  After  the
31700	application  of  the  Fourier  transform  the  Hadamard  transform is
31800	applied to detect a pitch period or to get a smoothed spectrum.  This
31900	method  shows some positive aspects of the Hadamard transform for the
32000	analysis of a speech wave with regard to the reduction of  processing
32100	time required for smoothing, but at the cost of precision.  A formant
32200	tracking program for voiced  speech  is  implemented  by  using  this
32300	method and an edge following technique used in scene analysis.
32400	
32500	
32600	AIM-176, Feldman, J.A.,  Low, J.R.,  Swinehart, D.C.,  Taylor, R. H.,
32700	         RECENT DEVELOPMENTS IN SAIL.  AN ALGOL-BASED  LANGUAGE  FOR
32800	         ARTIFICIAL INTELLIGENCE, (forthcoming).
32900	
33000	AIM-177, Paul,   Richard,   MODELLING,  TRAJECTORY  CALCULATION  AND
33100	         SERVOING OF A COMPUTER CONTROLLED ARM, (forthcoming)
33200	
33300	
33400	AIM-178,  Aharon Gill,   VISUAL  FEEDBACK  AND  RELATED  PROBLEMS  IN
33500	        COMPUTER  CONTROLLED  HAND  EYE  COORDINATION, October 1972,
33600		134 pages.
33700	
33800	A set of programs for precise manipulation of simple  planar  bounded
33900	objects,  by  means  of visual feedback, was developed for use in the
34000	Stanford hand-eye system.  The  system  includes  a  six  degrees  of
34100	freedom  computer  controlled  manipulator (arm and hand) and a fully
34200	instrumented computer television camera.
34300	
34400	The  image  of  the  hand  and manipulated objects is acquired by the
34500	computer through the camera.  The stored image is  analyzed  using  a
34600	corner  and  line  finding  program  developed for this purpose.  The
34700	analysis is simplified by using all the information  available  about
34800	the  objects  and  the  hand,  and  previously  measured coordination
34900	errors.   Simple  touch  and  force  sensing  by  the  arm  help  the
35000	determination of three dimensional positions from one view.
35100	
35200	The  utility  of  the information used to simplify the scene analysis
35300	depends on the accuracy of the geometrical models of the  camera  and
35400	arm.   A  set  of  calibration  updating  techniques and programs was
35500	developed to maintain the accuracy of the camera model relative to
35600	the arm model.
35700	
35800	The precision obtained is better than .1 inch.  It is limited by  the
35900	resolution of the imaging system and of the arm position measuring
36000	system.
36100	
36200	
36300	
36400	AIM-179, Baumgart, Bruce G.,  WINGED  EDGE POLYHEDRON REPRESENTATION, 
36500	         October 1972, 46 pages.
36600	
36700	(forthcoming)
36800	
36900	
37000	AIM-180, Bajcsy, Ruzena,  COMPUTER  IDENTIFICATION OF TEXTURED VISUAL
37100	         SCENES, October 1972, 156 pages.
37200	
37300	This work deals with computer analysis  of  textured  outdoor  scenes
37400	involving grass, trees, water and clouds. Descriptions of texture are
37500	formalized from natural language descriptions; local descriptors  are
37600	obtained  from  the directional and non-directional components of the
37700	Fourier transform power spectrum. Analytic expressions  are  obtained
37800	for  orientation, contrast, size, spacing, and in periodic cases, the
37900	locations of texture elements.  These local descriptors  are  defined
38000	over  windows  of  various  sizes;  the  choice of sizes is made by a
38100	simple higher-level program.
38200	
38300	The  process  of region growing is represented by a sheaf-theoretical
38400	model which formalizes the operation of pasting local structure (over
38500	a  window)  into  global  structure  (over  a  region). Programs were
38600	implemented which form regions of similar color and  similar  texture
38700	with respect to the local descriptors.
38800	
38900	An interpretation is made of texture gradient as  distance  gradient
39000	in  space.   A simple world model is described.  An interpretation of
39100	texture regions  and  texture  gradient  is  made  with  a  simulated
39200	correspondence  with the world model.  We find that a problem-solving
39300	approach, involving hypothesis-verification, more  satisfactory  than
39400	an  earlier pattern recognition effort (Bajcsy 1970) and more crucial
39500	to work with complex scenes than in scenes of  polyhedra.   Geometric
39600	clues  frPGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8PGA8